POPL 2020 (series) / Research Papers /
Par means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs
Fri 24 Jan 2020 12:07 - 12:30 at Ile de France II (IDF II) - Concurrent Programming & Session Types Chair(s): Susmit Sarkar
Along the lines of Abramsky’s “Proofs-as-Processes” program, we present an interpretation of multiplicative linear logic as typing system for concurrent functional programming. In particular, we study a linear multiple-conclusion natural deduction system and show it is isomorphic to a simple and natural extension of λ-calculus with parallelism and communication primitives, called λ_{par}. We shall prove that λ_{par} satisfies all the desirable properties for a typed programming language: subject reduction, progress, strong normalization and confluence.
Fri 24 JanDisplayed time zone: Saskatchewan, Central America change
Fri 24 Jan
Displayed time zone: Saskatchewan, Central America change
11:45 - 12:30 | Concurrent Programming & Session TypesResearch Papers at Ile de France II (IDF II) Chair(s): Susmit Sarkar University of St. Andrews | ||
11:45 22mTalk | Label-Dependent Session Types Research Papers Link to publication DOI Media Attached | ||
12:07 22mTalk | Par means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs Research Papers Link to publication DOI Media Attached |