Disjunctive Axioms and Concurrent $\lambda$-Calculi: a Curry-Howard Approach

TL;DR

This paper introduces a family of typed concurrent lambda calculi derived from classical disjunctive tautologies via the Curry-Howard correspondence, enabling advanced communication and code mobility features.

Contribution

It extends intuitionistic logic with disjunctive tautologies and develops new concurrent lambda calculi with unique communication mechanisms and code mobility, providing a computational interpretation for intermediate logics.

Findings

New typed concurrent lambda calculi with communication features

Implementation of code mobility in lambda calculus

First computational interpretation for many propositional intermediate logics

Abstract

We add to intuitionistic logic infinitely many classical disjunctive tautologies and use the Curry--Howard correspondence to obtain typed concurrent $\lambda$-calculi; each of them features a specific communication mechanism, including broadcasting and cyclic message-exchange, and enhanced expressive power with respect to the $\lambda$-calculus. Moreover they all implement forms of code mobility. Our results provide a first concurrent computational interpretation for many propositional intermediate logics, classical logic included.