Lambda the Ultimate

Replaced pre by blockquote, so now it has about 150 characters per line on my laptop :-)

I am not sure I understand. I get the long lines when pre is used. With blockquote lines wrap where they should...

I guess it depends on the resolution of the display and other settings. At 1400x1050 I get really wide and shallow articles - 150 characters per line is not an exaggeration. The current state of the web is not very friendly towards displays with such resolution (and no, setting bigger fonts in preferences does not work on all sites, as many sites prefer to enforce absolute sizes - LtU being a rare exception). Ah, nevermind...

Googling shows the seminal paper is tied up with the ACM (pay to view, etc.). Is there another introduction worth reading?

Do you mean Abstracting Control? Or A Functional Abstraction of Typed Contexts?

Griffin [22] pointed out that, just as the pure λ-calculus corresponds to intuitionistic logic, a λ-calculus with first-class continuations corresponds to classical logic. We study how first-class delimited continuations [13], in the form of Danvy and Filinski’s shift and reset operators [10, 11], can also be logically interpreted.

I am not sure I even buy the first paragraph, or really understand why it would be interesting to investigate. Guess I'll read up on that reference.

[Scanned the reference; I've seen it before. I don't buy it.]

Well, I really need to respond to CC Shan's comment, but that's going to take a few days of work. I'll handle yours first as it's a lot easier.

The idea is not too difficult: to be precise, if you start with the simply-typed lambda calculus without computational effects, a given type is inhabited if and only if that type is also a theorem of intuitionistic propositional logic, which does not accept the law of the excluded middle as legitimate. If you add call/cc, which can be typed with Peirce's law, then a type is inhabited if and only if it's a theorem of classical propositional logic.

Basically, these languages are sound and complete proof systems for the respective logics. As to why this is useful, I have some intuition, but it's vague and incomplete.

Of course, the simply-typed lambda calculus is strongly normalizing, (approximately speaking, expressions always terminate with an answer), and adding computational effects such as general recursion throws a monkey wrench into things.

For example, in Haskell, the simplest fixpoint operator has the following type:

fix :: (a -> a) -> a
fix f = let x = f x in x

bot :: a
bot = fix id

By simply claiming fix id as your "proof", you can prove anything you want. (i.e. everything) So you have to tread carefully, and you need to prove that your "proof" always terminates before it's type can really be accepted as a theorem.

Even though computational effects create problems, it's not the end of the Curry-Howard correspondence. In the simply typed lambda calculus with general recursion, for example, if your type is not a theorem of intuitionistic logic, then there are circumstances where your expression will not terminate. (Although the inverse statement is obviously not true.)

I hope that's enough to convince you as to why it's interesting, however I myself would love to hear about further practical applications of all this. Somebody more knowledgeable should correct me where I'm wrong, and expand on these statements.

You should also read the extra comment in the conclusion of [22].

[Accepting Peirce Law is accepting the excluded middle, as far as I understood.]

[If you add call/cc, which can be typed with Peirce's law, then a type is inhabited if and only if it's a theorem of classical propositional logic. .... sigh ]