# $\unicode{8523}$ means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs

## TL;DR

This paper interprets multiplicative linear logic as a typing system for concurrent functional programming, introducing a new calculus that supports parallelism and communication with desirable language properties.

## Contribution

It presents a novel extension of lambda calculus, called λ⊗, that models concurrent computation based on linear logic proofs, with formal proofs of key language properties.

## Key findings

- λ⊗ satisfies subject reduction and progress
- The calculus is strongly normalizing and confluent
- Provides a logical foundation for concurrent programming languages

## 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 $\lambda$-calculus with parallelism and communication primitives, called $\lambda_{\unicode{8523}}$. We shall prove that $\lambda_{\unicode{8523}}$ satisfies all the desirable properties for a typed programming language: subject reduction, progress, strong normalization and confluence.