Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.29736

Two Sides of the Same Proof: Extraction and Projection in Choreographic Programming

Matteo Acclavio·Giulia Manara·Fabrizio Montesi·Marco Peressotti
View original source ↗Read source document ↗Export metadata ↓

Abstract

A new approach to the theory of choreographic languages has recently been proposed, based on the interpretation of choreographies with finite behaviors as proofs in an extension of linear logic. This paper further develops this approach to cyclic proofs to be capable of representing infinite behaviors, and prove a completeness result for choreographies with respect to the class of lock-free networks. We show that in a choreographies-as-proofs correspondence, the proof equivalence induced by rule permutations corresponds to bisimilarity, and that, under adequate assumption on the procedure definitions, the proof search procedure has a finite search space, and can be used to extract a choreography from a network.

Explore related subjects

cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Matteo Acclavio, Giulia Manara, Fabrizio Montesi, Marco Peressotti. 2026-10-21. Two Sides of the Same Proof: Extraction and Projection in Choreographic Programming. https://arxiv.org/abs/2610.29736

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

A declarative approach to specifying Paxos using three-valued modal fixpoint logic

We present Three-valued Fixpoint Quorum Logic, or 3muQL for short; a three-valued modal fixed-point logic designed for declaratively specifying and reasoning about distributed algorithms, such as the Paxos consensus algorithm. Our methodology represents a distributed algorithm as a logical theory, enabling correctness properties to be derived directly within the framework -- or revealing logical errors in the algorithm's design when they exist. 3muQL adopts a declarative approach, specifying the overall logic of computation without prescribing control flow. Notably, message-passing and state-transitions are not explicitly modelled, and notions of 'quorum' are abstracted from concrete thresholds to abstract modal operators. This distinguishes our framework from approaches like TLA+. The logical abstraction emphasises the essence of distributed algorithms, offering a novel perspective on their specification and reasoning. We define the syntax and semantics of 3muQL, explore its theoretical properties, and demonstrate its applicability through a detailed treatment of the Paxos consensus algorithm. By presenting Paxos as a logical theory and deriving its standard correctness properties, we showcase the framework's capacity to handle non-trivial distributed systems. We envision 3muQL as a versatile tool for specifying and reasoning about distributed algorithms. The Paxos example highlights the framework's ability to capture intricate details, offering a new lens through which distributed algorithms can be specified, studied, and checked. The ideas we present are easily implemented, and to demonstrate this we have implemented a freely-available proof-of- concept 3muQL model-checker, as an effective prototyping tool.

cs.LO↗
arXiv2026

Ohana trees, linear approximation and multi-types for the $λ$I-calculus: No variable gets left behind or forgotten!

Although the $λ$I-calculus is a natural fragment of the $λ$-calculus, obtained by forbidding the erasure of arguments, its equational theories did not receive much attention. The reason is that all proper denotational models studied in the literature equate all non-normalizable $λ$I-terms, whence the associated theory is not very informative. The goal of this paper is to introduce a previously unknown theory of the $λ$I-calculus, induced by a notion of evaluation trees that we call "Ohana trees". The Ohana tree of a $λ$I-term is an annotated version of its Böhm tree, remembering all free variables that are hidden within its meaningless subtrees, or pushed into infinity along its infinite branches. We develop the associated theories of program approximation: the first approach -- more classic -- is based on finite trees and continuity, the second adapts Ehrhard and Regnier's Taylor expansion. We then prove a Commutation Theorem stating that the normal form of the Taylor expansion of a $λ$I-term coincides with the Taylor expansion of its Ohana tree. As a corollary, we obtain that the equality induced by Ohana trees is compatible with abstraction and application. Subsequently, we introduce a denotational model designed to capture the equality induced by Ohana trees. Although presented as a non-idempotent type system, our model is based on a suitably modified version of the relational semantics of the $λ$-calculus, which is known to yield proper models of the $λ$I-calculus when restricted to non-empty finite multisets. To track variables occurring in subterms that are hidden or pushed to infinity in the evaluation trees, we generalize the system in two ways: first, we reintroduce annotated versions of the empty multiset indexed by sets of variables; second, (...)

cs.LO↗
arXiv2026

A simple formalization of alpha-equivalence

While teaching untyped $λ$-calculus to undergraduate students, we were wondering why $α$-equivalence is not directly inductively defined. In this paper, we demonstrate that this is indeed feasible. Specifically, we provide a grounded, inductive definition for $α$-equivalence and show that it conforms to the specification provided in the literature. The work presented in this paper is fully formalized in the Rocq Prover.

cs.LO↗