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.

@article{paperbot523,
  title = {Par means parallel: multiplicative linear logic proofs as concurrent functional programs},
  author = {Federico Aschieri and Francesco A. Genco},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {4},
  number = {POPL},
  year = {2019},
  doi = {10.1145/3371086}
}