Disjunctive Axioms and Concurrent λ-Calculi: a Curry-Howard Approach

2018/02/03 by Federico Aschieri, Aschieri, F., Agata Ciabattoni +3
Computer Science · #Advanced Algebra and Logic #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #semigroups and automata theory

paper · pdf · doi:10.48550/arxiv.1802.00961

openalex publication_date 2018/02/03 · openalex created_date 2018/02/23 · openalex updated_date 2026/07/28

Abstract

We add to intuitionistic logic infinitely many classical disjunctive tautologies and use the Curry--Howard correspondence to obtain typed concurrent λ-calculi; each of them features a specific communication mechanism, including broadcasting and cyclic message-exchange, and enhanced expressive power with respect to the λ-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.

Related

• A typed parallel λ-calculus via 1-depth intermediate proofs
• Formalizing the Curry-Howard Correspondence
• The Many Worlds of Modal \λ-calculi: I. Curry-Howard for\n Necessity, Possibility and Time
• \unicode8523 means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs
• Interpreting a concurrent λ-calculus in differential proof nets (extended version)