8523 means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs
share
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 λ_8523. We shall prove that λ_8523 satisfies all the desirable properties for a typed programming language: subject reduction, progress, strong normalization and confluence.
READ FULL TEXT