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

Matteo Acclavio; Giulia Manara; Fabrizio Montesi; Marco Peressotti

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

BibTeX RIS

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

Formula size game and model checking for modal substitution calculus

Recent research has applied modal substitution calculus (MSC) and its variants to characterize various computational frameworks such as graph neural networks (GNNs) and distributed computing systems. For example, it has been shown that floating-point recurrent graph neural networks have the same expressive power as graded modal substitution calculus GMSC, which is the extension of MSC with counting modalities. GMSC can be further extended with the counting global modality, resulting in the logic GGMSC, which corresponds to floating-point GNNs with global readout mechanisms. In this paper, we introduce a formula size game that characterizes the expressive power of MSC, GMSC, GGMSC, and related logics. Furthermore, we study the expressiveness and model checking of logics in this family. We prove that MSC and its extensions (GMSC, GGMSC) are as expressive as linear tape-bounded Turing machines, while asynchronous variants are linked to the modal mu-calculus and modal computation logic MCL. We establish that for MSC, GMSC and GGMSC, both the combined and data complexity of model checking are PSPACE-complete, and for their asynchronous variants, both complexities are PTIME-complete. We also establish that for the propositional fragment SC of MSC, the combined complexity of model checking is PSPACE-complete, while for asynchronous SC it is PTIME-complete, and in both cases, the data complexity is constant. As a corollary, we observe that SC satisfiability is PSPACE-complete and NP-complete for its asynchronous variant. Finally, we construct a universal reduction from all recursively enumerable problems to MSC model checking.

cs.LO↗

arXiv2026

Theorem prover Arend

This paper is an exposition of the theorem prover Arend developed at JetBrains Research. Arend language has been designed to facilitate the formalization of mathematics within the framework of univalent foundations and with the focus on constructive mathematics. It is based on a variant of homotopy type theory with cubical syntax that is more closely aligned with Martin-Löf Type Theory (MLTT) than fully computational cubical type theories, while still retaining some of their computational properties useful in practice. Among the most notable features of the Arend language is its powerful system of classes and records supporting subsumptive subtyping, partial implementations and anonymous extensions, which provides extensive flexibility for constructing hierarchies of definitions. Formalization in Arend is streamlined by the IntelliJ Arend plugin, which transforms IntelliJ IDEA into a full-fledged integrated development environment (IDE) for the Arend language. The main Arend library arend-lib includes formalizations in constructive algebra, topology and synthetic homotopy theory.

cs.LO↗

arXiv2026

Post-Pruning vs. Early Stopping: Which Works Better for Link Prediction with AnyBurl?

Rule-based link prediction combines symbolic and statistical artificial intelligence methods by inductively learning a set of rules from a knowledge graph (KG), with the aim of completing the graph when a query cannot be answered from the KG alone. Several systems have been proposed, and while they perform well on classical benchmarks, even compared with embedding-based systems, many of them produce a large number of rules. This compromises scalability in the query-answering phase, especially under strong hardware constraints. In this work, we investigate the behavior of AnyBurl, a state-of-the-art rule learner for link prediction, to determine whether running it for a given time and then pruning the learned rules yields better query-answering performance at test time than a simpler approach that stops rule generation earlier.

cs.LO↗