Lambda the Ultimate

If Curry-Howard is your thing, you'll like this: Propositions as Sessions by Philip Wadler.

Continuing a line of work by Abramsky (1994), by Bellin and Scott (1994), and by Caires and Pfenning (2010), among others, this paper presents CP, a calculus in which propositions of classical linear logic correspond to session types. Continuing a line of work by Honda (1993), by Honda, Kubo, and Vasconcelos (1998), and by Gay and Vasconcelos (2010), among others, this paper presents GV, a linear functional language with session types, and presents a translation from GV into CP. The translation formalises for the first time a connection between a standard presentation of session types and linear logic, and shows how a modification to the standard presentation yield a language free from deadlock, where deadlock freedom follows from the correspondence to linear logic.

I was unable to find much LTU discussion about session types; they express the protocol that a process speaks over a channel [conjunction describes multistep conversations; disjunction offers a choice between different interactions, e.g. buy an item vs. quote its price --- you can see the type for this in Caires and Pfenning]. Instead of applying functions, one creates a channel and puts processes on either end of it. The types ensure that when one side of the channel is pushing output, the other side is reading input. This dual relationship between input/output corresponds with the dual (linear negation) in linear logic. Proof reduction (cut elimination) simulates communication between processes.

As λ-calculus provided foundations for functional programming in the last century, may we hope for this emerging calculus to provide foundations for concurrent programming in the coming century?