"Focusing proofs and the Curry-Howard correspondence" Everyone loves the Curry-Howard correspondence between programs and proofs...but how strongly do we really believe it? When we program in real-world functional languages, we encounter many "extra-logical" features, which it is tempting to sweep under the rug. Typically, a deterministic evaluation strategy is seen as a necessary evil; pattern-matching is a nice amenity for programmers, but certainly not something you would want in your proof/type theory; the "value restriction" on polymorphism in SML/O'Caml is a gross hack. In this talk, I will try to make the case that as devotees of Curry-Howard, we should not ignore these aspects of practical programming---remarkably, they all emerge out of a careful analysis of Andreoli's focusing proofs, using ideas from polarized logic and ludics. Moreover, rather than these real-world features adding blemishes to the proof theory, they actually simplify it considerably. In particular, we can define a focusing sequent calculus using a form of iterated inductive definition, which allows the identity and cut-elimination procedures to be expressed in a completely modular way, without mentioning any connectives. Positive connectives are defined inductively by their constructor patterns, negative connectives by their destructor patterns, and pattern-matching corresponds to an analogue of Buchholz' Omega-rule.