Lambda the Ultimate

writing a book, entitled Proof and Counterexample (or PnC for short). It's on logic viewed through the lens of proof theory. In particular, it covers natural deduction, sequent calculus, normalisation and cut-elimination. It's designed to both be state-of-the-art reseearch on these topics, together with an introduction appropriate for an advanced undergraduate. (We'll see how that works. I'll be test-driving the material with honours students from February to June in 2005.)

These pages will contain all sorts of different material about the book: comments, discussion, pointers to related material, and anything else that the community behind this site sees fit to write.

Newcomers to the field might wonder why this is relevant to programming languages, and some readers would regard this as pointless theory...

But if you are one of us guys excited by Curry-Howard, you might enjoy this wiki a lot.

This is a tutorial on using type-indexed embedding projection pairs when writing interpreters in statically-typed functional languages. The method allows (higher-order) values in the interpreting language to be embedded in the interpreted language and values from the interpreted language may be projected back into the interpreting one. This is particularly useful when adding command-line interfaces or scripting languages to applications written in functional languages. We first describe the basic idea and show how it may be extended to languages with recursive types and applied to elementary meta-programming. We then show how the method combines with Filinski's continuation-based monadic reflection operations to define an extensional version of the call-by-value monadic translation and hence to allow values to be mapped bidirectionally between the levels of an interpreter for a functional language parameterized by an arbitrary monad. Finally, we show how SML functions may be embedded into, and projected from, an interpreter for an asynchronous pi-calculus via an extensional variant of a standard translation from lambda into pi.

Another paper from Nick Benton.

Like the previous one this paper is dense and detailed, but this time there are some useful practical techniques that may come handy next time you build a DSL in a functional language.