Lambda the Ultimate

POPL 2007 is just around the corner, and the Little Calculist has taken time off from inventing Web 4.0 to track down all the papers available online, and collect them in an annotated program, Favourite titles: Proving That Programs Eventually Do Something Good, and Lazy Multivariate Higher-Order Forward-Mode AD. I have no idea what the later means, but I love the pile-up of jargon.

We provide a functional specification of three central components of Simon Peyton Jones’s awkward squad: teletype I/O, mutable state and concurrency. By constructing an internal model of such concepts within our programming language, we can reason about programs that perform I/O as if they were pure functions. One important application of our approach is accommodating I/O in a dependently typed programming language.