Classical Proofs as Parallel Programs

Abstract

We introduce a first proofs-as-parallel-programs correspondence for classical logic. We define a parallel and more powerful extension of the simply typed lambda calculus corresponding to an analytic natural deduction based on the excluded middle law. The resulting functional language features a natural higher-order communication mechanism between processes, which also supports broadcasting. The normalization procedure makes use of reductions that implement novel techniques for handling and transmitting process closures.

In Proceedings GandALF 2018, arXiv:1809.02416. arXiv admin note: text overlap with arXiv:1607.05120