Lambda the Ultimate

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.