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 Jan Times are displayed in time zone: Saskatchewan, Central America change
Fri 24 Jan
Times are displayed in 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 SarkarUniversity of St. Andrews | |||
11:45 - 12:07 Talk | Label-Dependent Session Types Research Papers Link to publication DOI Media Attached | ||
12:07 - 12:30 Talk | Par means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs Research Papers Link to publication DOI Media Attached |