Lambda the Ultimate

Right: I see that it might not be obvious. This is not a programming language theory paper, and one should not be thinking along the lines of "what would a Haskell look like that included this typed lambda calculus?" Rather, this is a significant recent contribution to the so-called classical Curry-Howard correspondence. I think I can make good the justification gap by providing an annotated bibliography of the most significant work since Curien and Herbelin's The Duality of Computation, but I haven't time to do that right now. I can make a few comments here, though:

1. I don't accept that either this paper, or Michel Parigot's strangely neglected 1997 article Strong Normalization of Second Order Symmetric lambda-Calculus, provides a Curry-Howard correspondence, since they are non-confluent calculi, and the Curry-Howard correspondence depends upon Prawitz's thesis, that the value of a proof is its normal form;
2. However, among other reasons, these calculi are significant in that they give rise to many interesting Curry-Howard calculi by restricting their rewrite relation. Going from symmetric calculi to asymmetric calculi is understood, an active area of new, interesting work, and is the technology behind Wadler's Call-by-value is dual to call-by-name;
3. And in general, these results are tricky: when you take an intuitionistic impredicative lambda-calculus and add constructions and rewrite rules to make it classical, one necessarily obtains a calculus that is harder to prove strong normalisation for than the original, and if you make that calculus symmetric, it becomes harder still. These are mother SN results, from which all kinds of other useful SN results follow by embedding translations.

To summarise, this is a theory paper that does not directly address PL design, but does increase the resources available to PL designers who want good type theories for their languages.

Posctscript: David and Nour's 2005 article Why the usual candidates of reducibility do not
work for the symmetric λμ-calculus helps understand the difficulties proving SN for such symmetric classical calculi; section 3.4 of my DPhil gives a different, earlier, account: my calculus is not symmetric, but has some mu-bar like rules for natural numbers induction, and so runs into the same difficulties.

As I get it, this is a SN result for a new type-theory which some kind of hybrid between an intuitionistic and a classical type theory.

Why did they take that route, what does it help, or maybe even, for those of use who are new to this: Why is a SN result interesting?

marco asked: Why is a SN result interesting? — which I missed at the time...

Essentially, a term rewriting system needs CR if we are to consider it a sane candidate as the basis for a functional programming language. SN is not necessary for this, but one can identify subsets, kernels if you like, of the rewriting system that provide the basis of the administrative core of the programming language: things like definitions, non-recursive control structures, non-recursive function applications, etc.

If you want to use some extension of the lambda calculus as the foundation for some FPL with first-class continuations, then first you need to identify a reduction strategy —or at least some constraint on possible rewrites— in the FPL that corresponds to a CR subsystem of your extended lambda calculus; and this subsystem needs to support everything in the FPL that deals with first-class continuations, and it needs to be SN.

Is that intelligible? Given one accepts that, then it should follow that the CR subsystems of Lengrand & Miquel's calculus are very interesting to those who follow the "classical formulae-as-types" literature.