Lolliproc: to concurrency from classical linear logic via curry-howard and control

While many type systems based on the intuitionistic fragment of linear logic have been proposed, applications in programming languages of the full power of linear logic--including double-negation elimination--have remained elusive. Meanwhile, linearity has been used in many type systems for concurrent programs--e.g., session types--which suggests applicability to the problems of concurrent programming, but the ways in which linearity has interacted with concurrency primitives in lambda calculi have remained somewhat ad-hoc. In this paper we connect classical linear logic and concurrent functional programming in the language Lolliproc, which provides simple primitives for concurrency that have a direct logical interpretation and that combine to provide the functionality of session types. Lolliproc features a simple process calculus "under the hood" but hides the machinery of processes from programmers. We illustrate Lolliproc by example and prove soundness, strong normalizati...

• Type: Conference
• Year: 2010
• Where: ICFP
• Authors: Karl Mazurak, Steve Zdancewic
• Keywords: ICFP 2010, Linear Logic, Programming Languages, Session Types, Type Systems