Classical Proofs as Parallel Programs

TL;DR

This paper establishes a novel correspondence between classical proofs and parallel programs, introducing an advanced lambda calculus with higher-order communication and broadcasting, enhancing the understanding of proof-program relationships.

Contribution

It presents the first proofs-as-parallel-programs correspondence for classical logic, extending the simply typed lambda calculus with new communication and normalization techniques.

Findings

Develops a parallel extension of the simply typed lambda calculus.

Introduces a natural higher-order communication mechanism.

Provides normalization techniques for process closures.

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.