Rémi Di Guardia ; Olivier Laurent - Type Isomorphisms for Multiplicative-Additive Linear Logic

lmcs:13088 - Logical Methods in Computer Science, November 21, 2025, Volume 21, Issue 4 - https://doi.org/10.46298/lmcs-21(4:24)2025
Type Isomorphisms for Multiplicative-Additive Linear LogicArticle

Authors: 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

    Consultation statistics

    This page has been seen 143 times.
    This article's PDF has been downloaded 120 times.