Lambda the Ultimate

(Link)

Here's something to exercise both brain hemispheres. Henk Barendregt needs no introduction for many LtU readers - he literally wrote "the book" on the lambda calculus, and that only hints at the profound impact his work has had on lambda calculus and type theory.

The page linked above lists two overlapping papers, both about reflection:

Reflection plays in several ways a fundamental role for our existence. Among other places the phenomenon occurs in life, in language, in computing and in mathematical reasoning. A fifth place in which reflection occurs is our spiritual development. In all of these cases the effects of reflection are powerful, even downright dramatic. We should be aware of these effects and use them in a responsible way.

A prototype situation where reflection occurs is in the so called lambda calculus. This is a formal theory that is capable of describing algorithms, logical and mathematical proofs, but also itself.

As the first paragraph quoted above implies, the scope of these two papers extends far beyond the lambda calculus, into fields such as biology and meditation. Between the two papers, there's something for everyone:

"Reflection and its use, from science to meditation" is wide-ranging, covering reflection related to living cells, formal languages, mathematics, art, computers, and the human mind.

"Reflection and its use, with an emphasis on languages and lambda calculus", focuses specifically on reflection in formal languages, including combinatory logic and lambda calculus.

I am off to bed, so I'll get back to this tomorrow per Luke's request.

For the time being I recommend section 2 of Wadler's Monads for functional programming.