\unicode8523 means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs

2019/07/08 by Aschieri, Federico, Genco, Francesco A.
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1907.03631

Abstract

Along the lines of the Abramsky ``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 λ_\unicode8523. We shall prove that λ_\unicode8523 satisfies all the desirable properties for a typed programming language: subject reduction, progress, strong normalization and confluence.

Related

• Gödel Logic: from Natural Deduction to Parallel Computation
• A typed parallel λ-calculus via 1-depth intermediate proofs
• On the Expressivity of Typed Concurrent Calculi
• Functions as proofs as processes
• Multirole Logic and Multiparty Channels