Type Isomorphisms for Multiplicative-Additive Linear Logic
<|reference_start|>Type Isomorphisms for Multiplicative-Additive Linear Logic: 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.<|reference_end|>
@article{di guardia2024type,
    title={Type Isomorphisms for Multiplicative-Additive Linear Logic},
    author={R'emi Di Guardia (LIP, PLUME), Olivier Laurent (LIP, PLUME)},
    journal={arXiv preprint arXiv:2402.11987},
    year={2024},
    archivePrefix={arXiv},
    eprint={2402.11987},
    primaryClass={cs.LO}
}