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

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
22m
Talk
Label-Dependent Session Types
Research Papers
Peter Thiemann University of Freiburg, Germany, Vasco T. Vasconcelos University of Lisbon, Portugal
Link to publication DOI Media Attached
12:07
22m
Talk
Par means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs
Research Papers
Federico Aschieri TU Wien, Francesco A. Genco IHPST, Université Paris 1
Link to publication DOI Media Attached