Type Isomorphisms for Multiplicative-Additive Linear LogicArticle
Authors: Rémi Di Guardia ; Olivier Laurent
NULL##NULL
Rémi Di Guardia;Olivier Laurent
We characterize type isomorphisms in the multiplicative-additive fragment of linear logic (MALL), and thus in *-autonomous categories with finite products, extending a result for the multiplicative fragment by Balat and Di Cosmo. This yields a much richer equational theory involving distributivity and cancellation laws. The unit-free case is obtained by relying on the proof-net syntax introduced by Hughes and Van Glabbeek. We use the sequent calculus to extend our results to full MALL, including all units, thanks to a study of cut-elimination and rule commutations.
Volume: Volume 21, Issue 4
Published on: November 21, 2025
Accepted on: September 25, 2025
Submitted on: February 20, 2024
Keywords: Logic in Computer Science
Funding:
Source : OpenAIRE Graph- Reasoning with Circular proofs for Programming; Funder: French National Research Agency (ANR); Code: ANR-21-CE48-0019
- Quantitative Reasoning Methods for Probabilistic Logics; Funder: French National Research Agency (ANR); Code: ANR-20-CE48-0005
- Quantitative Reasoning Methods for Probabilistic Logics; Funder: French National Research Agency (ANR); Code: ANR-11-IDEX-0007
- Dynamic Versatile Semantics; Funder: French National Research Agency (ANR); Code: ANR-19-CE48-0010