一句话：将乘法线性逻辑证明解释为并发函数式程序的类型系统，并证明 λpar 的元理论性质。
论文沿 Abramsky 的“证明即进程”路线，研究如何把乘法线性逻辑用作并发函数式编程的类型系统。作者考察一个线性的多结论自然演绎系统，并构造带并行与通信原语的 λ 演算扩展 λpar，证明该证明系统与 λpar 同构。这一对应使逻辑证明可直接视为并发程序，证明归约对应程序计算。作者进一步证明 λpar 满足良类型语言所需的关键性质，包括主体归约（subject reduction）、进展、强规范化与合流，从而为并发函数式语言设计提供了逻辑基础。
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}
}