A typed parallel {\lambda}-calculus via 1-depth intermediate proofs

TL;DR

This paper presents a new typed parallel lambda-calculus, mbda_{\u2225}, based on 1-depth intermediate proofs, enabling modeling of complex parallel computations and process networks within a logical framework.

Contribution

It introduces mbda_{\u2225}, a strongly normalizing parallel lambda-calculus derived from a novel Curry-Howard correspondence for 1-depth intermediate logics, expanding the expressiveness of typed lambda-calculi.

Findings

mbda_{\u2225} models arbitrary process network topologies.

The calculus encodes a range of parallel programs, including numeric and graph algorithms.

It maintains strong normalization despite parallel extensions.

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.