Lambda the Ultimate

I mentioned this somewhat passingly a few years ago. So not to make the same mistake again, I'm reposting this as a top-level post (and with current links).

His list of publications and the recent ones. Some relatively recent work by him discussed on LtU is here.

The ones I want to highlight in particular are his applications of the Curry-Howard correspondence to machine code generation and such topics.