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.

@article{paperbot3346,
  title = {Type Isomorphisms for Multiplicative-Additive Linear Logic},
  author = {Rémi Di Guardia and Olivier Laurent},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 21, Issue 4},
  year = {2025},
  doi = {10.46298/lmcs-21(4:24)2025}
}