19/01/2020

Par means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs

Federico Aschieri, Francesco A. Genco

Keywords: Proofs-as-programs, classical multiplicative linear logic, concurrency

Abstract: 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.

 0
 0
 0
 0
This is an embedded video. Talk and the respective paper are published at POPL 2020 virtual conference. If you are one of the authors of the paper and want to manage your upload, see the question "My papertalk has been externally embedded..." in the FAQ section.

Comments

Post Comment
no comments yet
code of conduct: tbd

Similar Papers