Write a Blog >>

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 (GMT-06:00) Saskatchewan, Central America change

11:45 - 12:30: Research Papers - Concurrent Programming & Session Types at Ile de France II (IDF II)
Chair(s): Susmit SarkarUniversity of St. Andrews
POPL-2020-Research-Papers11:45 - 12:07
Peter ThiemannUniversity of Freiburg, Germany, Vasco T. VasconcelosUniversity of Lisbon, Portugal
Link to publication DOI Media Attached
POPL-2020-Research-Papers12:07 - 12:30
Federico AschieriTU Wien, Francesco A. GencoIHPST, Université Paris 1
Link to publication DOI Media Attached