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 normalization, and confluence results, which, among other things, guarantees freedom from deadlocks and race conditions.
Keywords for this software
References in zbMATH (referenced in 5 articles , 1 standard article )
Showing results 1 to 5 of 5.
- Paykin, Jennifer; Zdancewic, Steve: Linear (\lambda\mu) is CP (more or less) (2016)
- Pérez, Jorge A.; Caires, Luís; Pfenning, Frank; Toninho, Bernardo: Linear logical relations and observational equivalences for session-based concurrency (2014)
- Pfenning, Frank; Caires, Luis; Toninho, Bernardo: Proof-carrying code in a session-typed process calculus (2011)
- -: Proceedings of the 15th ACM SIGPLAN international conference on functional programming, ICFP ’10, Baltimore, MD, USA, September 27--29, 2010 (2010)
- Mazurak, Karl; Zdancewic, Steve: Lolliproc: to concurrency from classical linear logic via Curry-Howard and control (2010)