Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

arXiv:2411.08847

Proofs as Execution Trees for the π-Calculus

Matteo Acclavio, Giulia Manara

Published Nov 13, 2024• 1 citation
arXivHTMLPDF

Abstract

In this paper, we establish the foundations of a novel logical framework for the π-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.

DOI
10.48550/arxiv.2411.08847

Related papers

An algebraic extension of intuitionistic linear logic: the 𝓛!𝒮-calculus and its categorical model

Alejandro Díaz-Caro, Malena Ivnisky, Octavio Malherbe

Abstract We introduce the ${{\mathcal L}_!^{\mathcal S}}$-calculus, a linear lambda-calculus extended with scalar multiplication and term addition, that acts as a proof language for intuitionistic linear logic. These algebraic operations enable the direct expression of linearity at the syntactic level, a property not typically available in standard proof-term calculi. Building upon previous work, we develop the ${{\mathcal L}_{!}^{\mathcal S}}$-calculus as an extension of the ${\mathcal L}^{\mathcal S}$-calculus with the ! modality. We prove key meta-theoretical properties—subject reduction, confluence, strong normalization and an introduction property—as well as preserve the expressiveness of the original ${\mathcal L}^{\mathcal S}$-calculus, including the encoding of vectors and matrices, and the correspondence between proof-terms and linear functions. A denotational semantics is provided in the framework of linear categories with biproducts, ensuring a sound and adequate interpretation of the calculus. This work is part of a broader programme aiming to build a measurement-free quantum programming language grounded in linear logic.

arXiv:2504.12128•Journal of Logic and Computation•Nov 4, 2025•0 citations

Sequent Calculus and Quantum Parallelism

Giulia Battilotti

In the last years, quantum computational logics have been developed in order to describe the logical setting of quantum computation [1]. An important challenge is the development of proof theoretical tools for quantum computation, so that the physical process of computation can correspond to a logical process of computation. In particular, the challenge is that quantum computational speed up, due to superposition and entanglement, can find an explanation in terms of logical proofs. The object of our research is a sequent calculus developed in the framework of basic logic, that is a logical platform to study extensional logics, including quantum logics [2, 3]. In basic logic, logical connectives and their rules are the result of importing suitable links at the metalevel into the object level. We suppose that a particular kind of dynamics between the object level and the metalevel is created when considering a quantum system rather than a classical one. This is due to a specific treatment of variables, that, in our view, can create the logical setting for a holistic, rather than compositional, treatment of information, proper of entangled states [4]. Then we develop a predicative sequent calculus. In it, superposition is built by quantifying a propo-sition, associated with a quantum system, on a first order domain determined by the experiments on such system. Then a convenient treatment of variables can create dynamically entangled states in logical

•Jan 7, 2015•0 citations

Generalised Proof-Nets for Compact Categories with Biproducts

Duncan, Ross

Just as conventional functional programs may be understood as proofs in an intuitionistic logic, so quantum processes can also be viewed as proofs in a suitable logic. We describe such a logic, the logic of compact closed categories and biproducts, presented both as a sequent calculus and as a system of proof-nets. This logic captures much of the necessary structure needed to represent quantum processes under classical control, while remaining agnostic to the fine details. We demonstrate how to represent quantum processes as proof-nets, and show that the dynamic behaviour of a quantum process is captured by the cut-elimination procedure for the logic. We show that the cut elimination procedure is strongly normalising: that is, that every legal way of simplifying a proof-net leads to the same, unique, normal form. Finally, taking some initial set of operations as non-logical axioms, we show that that the resulting category of proof-nets is a representation of the free compact closed category with biproducts generated by those operations.

arXiv:0903.5154•Mar 30, 2009•4 citations

Sequent Calculus Representations for Quantum Circuits

Cameron Beebe

When considering a sequent-style proof system for quantum programs, there are certain elements of quantum mechanics that we may wish to capture, such as phase, dynamics of unitary transformations, and measurement probabilities. Traditional quantum logics which focus primarily on the abstract orthomodular lattice theory and structures of Hilbert spaces have not satisfactorily captured some of these elements. We can start from 'scratch' in an attempt to conceptually characterize the types of proof rules which should be in a system that represents elements necessary for quantum algorithms. This present work attempts to do this from the perspective of the quantum circuit model of quantum computation. A sequent calculus based on single quantum circuits is suggested, and its ability to incorporate important conceptual and dynamic aspects of quantum computing is discussed. In particular, preserving the representation of phase helps illustrate the role of interference as a resource in quantum computation. Interference also provides an intuitive basis for a non-monotonic calculus.

arXiv:1606.06799•Electronic Proceedings in Theoretical Computer Science•Jun 20, 2016•0 citations

Generalized Proof-Nets for Compact Categories with Biproducts

Ross Duncan

Just as conventional functional programs may be understood as proofs in an intuitionistic logic, so quantum processes can also be viewed as proofs in a suitable logic.We describe such a logic, the logic of compact closed categories and biproducts, presented both as a sequent calculus and as a system of proof-nets. This logic captures much of the necessary structure needed to represent quantum processes under classical control, while remaining agnostic to the fine details. We demonstrate how to represent quantum processes as proof-nets and show that the dynamic behavior of a quantum process is captured by the cut-elimination procedure for the logic. We show that the cut-elimination procedure is strongly normalizing: that is, that every legal way of simplifying a proof-net leads to the same, unique, normal form. Finally, taking some initial set of operations as nonlogical axioms, we show that that the resulting category of proof-nets is a representation of the free compact closed category with biproducts generated by those operations. 3.1 Introduction 3.1.1 Logic, Processes, and Categories Birkhoff and von Neumann initiated the logical study of quantum mechanics in their well-known 1936 paper. They constructed a logic by assigning a proposition letter to each observable property of a given quantum system and studied negations, conjunctions, and disjunctions of these properties. The resulting lattice is nondistributive, and so the heart of what is called “quantum logic” is the study of various kinds of nondistributive lattices.

Cambridge University Press eBooks•Nov 30, 2009•4 citations

A categorical quantum logic

Samson Abramsky, ROSS DUNCAN

We define a strongly normalising proof-net calculus corresponding to the logic of strongly compact closed categories with biproducts. The calculus is a full and faithful representation of the free strongly compact closed category with biproducts on a given category with an involution. This syntax can be used to represent and reason about quantum processes.

arXiv:quant-ph/0512114•Mathematical Structures in Computer Science•Jun 1, 2006•31 citations
In this paper, we establish the foundations of a novel logical framework for the π-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.
Abstract We introduce the L!S{{\mathcal L}_!^{\mathcal S}}L!S​-calculus, a linear lambda-calculus extended with scalar multiplication and term addition, that acts as a proof language for intuitionistic linear logic. These algebraic operations enable the direct expression of linearity at the syntactic level, a property not typically available in standard proof-term calculi. Building upon previous work, we develop the L!S{{\mathcal L}_{!}^{\mathcal S}}L!S​-calculus as an extension of the LS{\mathcal L}^{\mathcal S}LS-calculus with the ! modality. We prove key meta-theoretical properties—subject reduction, confluence, strong normalization and an introduction property—as well as preserve the expressiveness of the original LS{\mathcal L}^{\mathcal S}LS-calculus, including the encoding of vectors and matrices, and the correspondence between proof-terms and linear functions. A denotational semantics is provided in the framework of linear categories with biproducts, ensuring a sound and adequate interpretation of the calculus. This work is part of a broader programme aiming to build a measurement-free quantum programming language grounded in linear logic.
In the last years, quantum computational logics have been developed in order to describe the logical setting of quantum computation [1]. An important challenge is the development of proof theoretical tools for quantum computation, so that the physical process of computation can correspond to a logical process of computation. In particular, the challenge is that quantum computational speed up, due to superposition and entanglement, can find an explanation in terms of logical proofs. The object of our research is a sequent calculus developed in the framework of basic logic, that is a logical platform to study extensional logics, including quantum logics [2, 3]. In basic logic, logical connectives and their rules are the result of importing suitable links at the metalevel into the object level. We suppose that a particular kind of dynamics between the object level and the metalevel is created when considering a quantum system rather than a classical one. This is due to a specific treatment of variables, that, in our view, can create the logical setting for a holistic, rather than compositional, treatment of information, proper of entangled states [4]. Then we develop a predicative sequent calculus. In it, superposition is built by quantifying a propo-sition, associated with a quantum system, on a first order domain determined by the experiments on such system. Then a convenient treatment of variables can create dynamically entangled states in logical
Just as conventional functional programs may be understood as proofs in an intuitionistic logic, so quantum processes can also be viewed as proofs in a suitable logic. We describe such a logic, the logic of compact closed categories and biproducts, presented both as a sequent calculus and as a system of proof-nets. This logic captures much of the necessary structure needed to represent quantum processes under classical control, while remaining agnostic to the fine details. We demonstrate how to represent quantum processes as proof-nets, and show that the dynamic behaviour of a quantum process is captured by the cut-elimination procedure for the logic. We show that the cut elimination procedure is strongly normalising: that is, that every legal way of simplifying a proof-net leads to the same, unique, normal form. Finally, taking some initial set of operations as non-logical axioms, we show that that the resulting category of proof-nets is a representation of the free compact closed category with biproducts generated by those operations.
When considering a sequent-style proof system for quantum programs, there are certain elements of quantum mechanics that we may wish to capture, such as phase, dynamics of unitary transformations, and measurement probabilities. Traditional quantum logics which focus primarily on the abstract orthomodular lattice theory and structures of Hilbert spaces have not satisfactorily captured some of these elements. We can start from 'scratch' in an attempt to conceptually characterize the types of proof rules which should be in a system that represents elements necessary for quantum algorithms. This present work attempts to do this from the perspective of the quantum circuit model of quantum computation. A sequent calculus based on single quantum circuits is suggested, and its ability to incorporate important conceptual and dynamic aspects of quantum computing is discussed. In particular, preserving the representation of phase helps illustrate the role of interference as a resource in quantum computation. Interference also provides an intuitive basis for a non-monotonic calculus.
Just as conventional functional programs may be understood as proofs in an intuitionistic logic, so quantum processes can also be viewed as proofs in a suitable logic.We describe such a logic, the logic of compact closed categories and biproducts, presented both as a sequent calculus and as a system of proof-nets. This logic captures much of the necessary structure needed to represent quantum processes under classical control, while remaining agnostic to the fine details. We demonstrate how to represent quantum processes as proof-nets and show that the dynamic behavior of a quantum process is captured by the cut-elimination procedure for the logic. We show that the cut-elimination procedure is strongly normalizing: that is, that every legal way of simplifying a proof-net leads to the same, unique, normal form. Finally, taking some initial set of operations as nonlogical axioms, we show that that the resulting category of proof-nets is a representation of the free compact closed category with biproducts generated by those operations. 3.1 Introduction 3.1.1 Logic, Processes, and Categories Birkhoff and von Neumann initiated the logical study of quantum mechanics in their well-known 1936 paper. They constructed a logic by assigning a proposition letter to each observable property of a given quantum system and studied negations, conjunctions, and disjunctions of these properties. The resulting lattice is nondistributive, and so the heart of what is called “quantum logic” is the study of various kinds of nondistributive lattices.