"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.