Lambda the Ultimate

Type Directed Concurrency by Deepak Garg and Frank Pfenning (2005)

Abstract. We introduce a novel way to integrate functional and concurrent programming based on intuitionistic linear logic. The functional core arises from interpreting proof reduction as computation. The concurrent core arises from interpreting proof search as computation. The two are tightly integrated via a monad that permits both sides to share the same logical meaning for the linear connectives while preserving their different computational paradigms. For example, concurrent computation synthesizes proofs which can be evaluated as functional programs. We illustrate our design with some small examples, including an encoding of the pi-calculus.

This paper doesn't seem to even have been mentioned on LtU before. Frank Pfenning is one of the computer scientists I watch and this is related to LolliMon and CLF which I find quite interesting. The language that results is very LolliMon/CLF-esque.