DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2023.26

Type Isomorphisms for Multiplicative-Additive Linear Logic

Authors: Rémi Di Guardia and Olivier Laurent

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract

We characterize type isomorphisms in the multiplicative-additive fragment of linear logic (MALL), and thus for ⋆-autonomous categories with finite products, extending a result for the multiplicative fragment by Balat and Di Cosmo [Vincent Balat and Roberto Di Cosmo, 1999]. This yields a much richer equational theory involving distributivity and annihilation laws. The unit-free case is obtained by relying on the proof-net syntax introduced by Hughes and Van Glabbeek [Dominic Hughes and Rob van Glabbeek, 2005]. We then use the sequent calculus to extend our results to full MALL (including all units).

Cite as

Rémi Di Guardia and Olivier Laurent. Type Isomorphisms for Multiplicative-Additive Linear Logic. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 26:1-26:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{diguardia_et_al:LIPIcs.FSCD.2023.26,
  author =	{Di Guardia, R\'{e}mi and Laurent, Olivier},
  title =	{{Type Isomorphisms for Multiplicative-Additive Linear Logic}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{26:1--26:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.26},
  URN =		{urn:nbn:de:0030-drops-180103},
  doi =		{10.4230/LIPIcs.FSCD.2023.26},
  annote =	{Keywords: Linear Logic, Type Isomorphisms, Multiplicative-Additive fragment, Proof nets, Sequent calculus, Star-autonomous categories with finite products}
}

Search Results

Documents authored by Di Guardia, Rémi

Type Isomorphisms for Multiplicative-Additive Linear Logic

Abstract

Cite as

Thanks for your feedback!

Could not send message