A typed parallel λ-calculus via 1-depth intermediate proofs

Abstract

We introduce a Curry-Howard correspondence for a large class of intermediate logics characterized by intuitionistic proofs with non-nested applications of rules for classical disjunctive tautologies (1-depth intermediate proofs). The resulting calculus, we call it ${\lambda }_{\parallel }$, is a strongly normalizing parallel extension of the simply typed $\lambda$-calculus. Although simple, the ${\lambda }_{\parallel }$ reduction rules can model arbitrary process network topologies, and encode interesting parallel programs ranging from numeric computation to algorithms on graphs.

LPAR23