arXiv subjects

Matteo Acclavio

Publications and source records attributed to Matteo Acclavio.

At least 19 recordsLinked to original sources

arXiv2026

Choreographic Programming: a Semantic Approach

The Endpoint Projection (EPP) theorem is a cornerstone of choreographic programming. It states that every choreography can be projected to a network of processes that correctly implements it. Proving EPP is notoriously difficult, and existing proofs are complex and non-modular because of the mismatch between the global view of choreographies and the local view of processes. In this article, we show how to reconcile this mismatch by designing a new semantics for choreographies that is built on the local view of processes, as well as a new preorder relation between choreographies and networks that extends bisimulation to deal with the propagation of knowledge of choice among distributed processes. As a result, we can give a modular proof of EPP, which is conceptually simpler than existing ones and also provides better insights on the theory of choreographic programming.

cs.PL↗

arXiv2026

Proof Nets for PiL (Full Version)

We introduce proof nets for PiL, an extension of first-order multiplicative additive linear logic with new operators allowing a shallow encoding of processes in the {\pi}-calculus as formulas. We provide correctness criterion, sequentialization procedure, and a proof translation algorithm. We show that proof nets provide a canonical representation of sequent calculus derivations modulo rule permutations.

cs.LO↗

arXiv2026

Proof Identity and Categorical Models of BV

BV-categories are a recent development that aims to give categorical semantics to proofs in the logic BV. However, due to the absence of a coherence theorem on one side and a well-defined notion of proof identity for BV on the other side, the precise relation between BV-categories and the logic BV is still not clear. To improve on this situation, we define in this paper a notion of proof identity for BV, based on the notion of atomic flows, which can be seen as a special form of string diagrams. Based on this notion of proof identity, we then strengthen the existing notion of BV-category and prove that it is sound with respect to the logic.

cs.LO↗

arXiv2026

Probabilistic Linear Logic Programming with an Application to Bayesian Network Computations (Extended Version)

Bayesian networks are a canonical formalism for representing probabilistic dependencies, yet their integration within logic programming frameworks remains a nontrivial challenge, mainly due to the complex structure of these networks. In this paper, we propose probLO (probabilistic Linear Objects) an extension of Andreoli and Pareschi's LO language which embeds Bayesian network representation and computation within the framework of multiplicative-additive linear logic programming. The key novelty is the use of multi-head Prolog-like methods to reconstruct network structures, which are not necessarily trees, and the operation of slicing, standard in the literature of linear logic, enabling internal numerical probability computations without relying on external semantic interpretation.

cs.LO↗

arXiv2025

Intuitionistic BV (Extended version)

We present the logic IBV, which is an intuitionistic version of BV, in the sense that its restriction to the MLL connectives is exactly IMLL, the intuitionistic version of MLL. For this logic we give a deep inference proof system and show cut elimination. We also show that the logic obtained from IBV by dropping the associativity of the new non-commutative seq-connective is an intuitionistic variant of the recently introduced logic NML. For this logic, called INML, we give a cut-free sequent calculus.

cs.LO↗

arXiv2025

Formulas as Processes, Deadlock-Freedom as Choreographies (Extended Version)

We introduce a novel approach to studying properties of processes in the {\pi}-calculus based on a processes-as-formulas interpretation, by establishing a correspondence between specific sequent calculus derivations and computation trees in the reduction semantics of the recursion-free {\pi}-calculus. Our method provides a simple logical characterisation of deadlock-freedom for the recursion- and race-free fragment of the {\pi}-calculus, supporting key features such as cyclic dependencies and an independence of the name restriction and parallel operators. Based on this technique, we establish a strong completeness result for a nontrivial choreographic language: all deadlock-free and race-free finite {\pi}-calculus processes composed in parallel at the top level can be faithfully represented by a choreography. With these results, we show how the paradigm of computation-as-derivation extends the reach of logical methods for the study of concurrency, by bridging important gaps between logic, the expressiveness of the {\pi}-calculus, and the expressiveness of choreographic languages.

cs.LO↗

arXiv2024

Proofs as Execution Trees for the {\pi}-Calculus

In this paper, we establish the foundations of a novel logical framework for the {\pi}-calculus, based on the deduction-as-computation paradigm. Following the standard proof-theoretic interpretation of logic programming, we represent processes as formulas, and we interpret proofs as computations. For this purpose, we define a cut-free sequent calculus for an extension of first-order multiplicative and additive linear logic. This extension includes a non-commutative and non-associative connective to faithfully model the prefix operator, and nominal quantifiers to represent name restriction. Finally, we design proof nets providing canonical representatives of derivations up to local rule permutations.

cs.LO↗

arXiv2024

Non-wellfounded parsimonious proofs and non-uniform complexity

In this paper we investigate the complexity-theoretical aspects of cyclic and non-wellfounded proofs in the context of parsimonious logic, a variant of linear logic where the exponential modality ! is interpreted as a constructor for streams over finite data. We present non-wellfounded parsimonious proof systems capturing the classes $\mathbf{FP}$ and $\mathbf{FP}/\mathsf{poly}$. Soundness is established via a polynomial modulus of continuity for continuous cut-elimination. Completeness relies on an encoding of polynomial Turing machines with advice within a type assignment system based on parsimonious logic. As a byproduct of our proof methods, we establish a series of characterisation results for various finitary proof systems.

cs.LO↗

arXiv2024

On Propositional Dynamic Logic and Concurrency

Dynamic logic is a powerful approach to reasoning about programs and their executions, obtained by extending classical logic with modalities that can express program executions as formulas. However, the use of dynamic logic in the setting of concurrency has proved problematic because of the challenge of capturing interleaving. This challenge stems from the fact that, traditionally, programs are represented by their sets of traces. These sets are then expressed as elements of a Kleene algebra, for which it is not possible to decide equality in the presence of the commutations required to model interleaving. In this work, we generalise propositional dynamic logic (PDL) to a logic framework we call operational propositional dynamic logic (OPDL), which departs from tradition by distinguishing programs from their traces. Traces are generated by an arbitrary operational semantics that we take as a parameter, making our approach applicable to different program syntaxes and semantics. To develop our framework, we provide the first proof of cut-elimination for a finitely-branching non-wellfounded sequent calculus for PDL. Thanks to this result we can effortlessly prove adequacy for PDL, and extend these results to OPDL. We conclude by discussing OPDL for two representative cases of concurrency: the Calculus of Communicating Systems (CCS), where interleaving is obtained by parallel composition, and Choreographic Programming, where interleaving is obtained by out-of-order execution.

cs.LO↗

arXiv2024

Logic Programming with Multiplicative Structures

In the logic programming paradigm, a program is defined by a set of methods, each of which can be executed when specific conditions are met during the current state of an execution. The semantics of these programs can be elegantly represented using sequent calculi, in which each method is linked to an inference rule. In this context, proof search mirrors the program's execution. Previous works introduced a framework in which the process of constructing proof nets is employed to model executions, as opposed to the traditional approach of proof search in sequent calculus. This paper further extends this investigation by focussing on the pure multiplicative fragment of this framework. We demonstrate, providing practical examples, the capability to define logic programming methods with context-sensitive behaviors solely through specific resource-preserving and context-free operations, corresponding to certain generalized multiplicative connectives explored in existing literature. We show how some of these methods, although still multiplicative, escape the purely multiplicative fragment of Linear Logic (MLL).

cs.LO↗

arXiv2023

Infinitary Cut-Elimination for Non-Wellfounded Parsimonious Linear Logic

We investigate non-wellfounded proof systems based on parsimonious logic, a weaker variant of linear logic where the exponential modality ! is interpreted as a constructor for streams over finite data. Logical consistency is maintained at a global level by adapting a standard progressing criterion. We present an infinitary version of cut-elimination based on finite approximations, and we prove that, in presence of the progressing criterion, it returns well-defined non-wellfounded proofs at its limit. Furthermore, we show that cut-elimination preserves the progressive criterion and various regularity conditions internalizing degrees of proof-theoretical uniformity. Finally, we provide a denotational semantics for our systems based on the relational model.

cs.LO↗

arXiv2023

Graphical Proof Theory I: Sequent Systems on Undirected Graphs

In this paper we explore the design of sequent calculi operating on graphs. For this purpose, we introduce a set of logical connectives allowing us to extend the correspondence between cographs and classical propositional formulas to any graph. We then provide sequent calculi operating on these formulas, we prove cut-elimination and that formula encoding the same graph are logically equivalent. We show that these systems provide conservative extensions of multiplicative linear logic (with and without mix) and classical propositional logic. We conclude by showing that one of these systems is equivalent to the graphical logic GS defined via a system of context-free graph rewiring rules, therefore providing an alternative proof of analyticity for this logic over graphs.

cs.LO↗

arXiv2023

Canonicity of Proofs in Constructive Modal Logic

In this paper we investigate the Curry-Howard correspondence for constructive modal logic in light of the gap between the proof equivalences enforced by the lambda calculi from the literature and by the recently defined winning strategies for this logic. We define a new lambda-calculus for a minimal constructive modal logic by enriching the calculus from the literature with additional reduction rules and we prove normalization and confluence for our calculus. We then provide a typing system in the style of focused proof systems allowing us to provide a unique proof for each term in normal form, and we use this result to show a one-to-one correspondence between terms in normal form and winning innocent strategies.

cs.LO↗

arXiv2021

Exponentially Handsome Proof Nets and Their Normalization

Handsome proof nets were introduced by Retoré as a syntax for multiplicative linear logic. These proof nets are defined by means of cographs (graphs representing formulas) equipped with a vertices partition satisfying simple topological conditions. In this paper we extend this syntax to multiplicative linear logic with units and exponentials. For this purpose we develop a new sound and complete sequent system for the logic, enforcing a stronger notion of proof equivalence with respect to the one usually considered in the literature. We then define combinatorial proofs, a graphical proof system able to capture syntactically the proof equivalence, for the cut-free fragment of the calculus. We conclude the paper by defining the exponentially handsome proof nets as combinatorial proofs with cuts and defining an internal normalization procedure for this syntax.

cs.LO↗

arXiv2021

A Deep Inference System for Differential Linear Logic

Differential linear logic (DiLL) provides a fine analysis of resource consumption in cut-elimination. We investigate the subsystem of DiLL without promotion in a deep inference formalism, where cuts are at an atomic level. In our system every provable formula admits a derivation in normal form, via a normalization procedure that commutes with the translation from sequent calculus to deep inference.

cs.LO↗

arXiv2021

Towards a Denotational Semantics for Proofs in Constructive Modal Logic

In this paper we provide two new semantics for proofs in the constructive modal logics CK and CD. The first semantics is given by extending the syntax of combinatorial proofs for propositional intuitionistic logic, in which proofs are factorised in a linear fragment (arena net) and a parallel weakening-contraction fragment (skew fibration). In particular we provide an encoding of modal formulas by means of directed graphs (modal arenas), and an encoding of linear proofs as modal arenas equipped with vertex partitions satisfying topological criteria. The second semantics is given by means of winning innocent strategies of a two-player game over modal arenas. This is given by extending the Heijltjes-Hughes-Straßburger correspondence between intuitionistic combinatorial proofs and winning innocent strategies in a Hyland-Ong arena. Using our first result, we provide a characterisation of winning strategies for games on a modal arena corresponding to proofs with modalities.

cs.LO↗

arXiv2020

An Analytic Propositional Proof System on Graphs

In this paper we present a proof system that operates on graphs instead of formulas. Starting from the well-known relationship between formulas and cographs, we drop the cograph-conditions and look at arbitrary undirected) graphs. This means that we lose the tree structure of the formulas corresponding to the cographs, and we can no longer use standard proof theoretical methods that depend on that tree structure. In order to overcome this difficulty, we use a modular decomposition of graphs and some techniques from deep inference where inference rules do not rely on the main connective of a formula. For our proof system we show the admissibility of cut and a generalisation of the splitting property. Finally, we show that our system is a conservative extension of multiplicative linear logic with mix, and we argue that our graphs form a notion of generalised connective.

cs.LO↗

arXiv2017

A Constructive Proof of Coherence for Symmetric Monoidal Categories Using Rewriting

A symmetric monoidal category is a category equipped with an associative and commutative (binary) product and an object which is the unit for the product. In fact, those properties only hold up to natural isomorphisms which satisfy some coherence conditions. The coherence theorem asserts the commutativity of all linear diagrams involving the left and right unitors, the associator and the braiding. We prove the coherence for symmetric monoidal categories using a homotopical method based on rewriting. For that scope, we detail the con vergence proof of Lafont's string diagram rewriting system which presents the isomorphisms of these theories.

math.CT↗