Search Results

Documents authored by Laurent, Olivier

Document
DOI: 10.4230/LIPIcs.FSCD.2025.16
Yeo’s Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic

Authors: Rémi Di Guardia, Olivier Laurent, Lorenzo Tortora de Falco, and Lionel Vaux Auclair

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
We revisit sequentialization proofs associated with the Danos-Regnier correctness criterion in the theory of proof nets of linear logic. Our approach relies on a generalization of Yeo’s theorem for graphs, based on colorings of half-edges. This happens to be the appropriate level of abstraction to extract sequentiality information from a proof net without modifying its graph structure. We thus obtain different ways of recovering a sequent calculus derivation from a proof net inductively, by relying on a splitting ⅋-vertex, on a splitting ⊗-vertex, on a splitting terminal vertex, etc. The proof of our Yeo-style theorem relies on a key lemma that we call cusp minimization. Given a coloring of half-edges, a cusp in a path is a vertex whose adjacent half-edges in the path have the same color. And, given a cycle with at least one cusp and subject to suitable hypotheses, cusp minimization constructs a cycle with strictly less cusps. In the absence of cusp-free cycles, cusp minimization is then enough to ensure the existence of a splitting vertex, i.e. a vertex that is a cusp of any cycle it belongs to. Our theorem subsumes several graph-theoretical results, including some known to be equivalent to Yeo’s theorem. The novelty is that they can be derived in a straightforward way, just by defining a dedicated coloring, again without any modification of the underlying graph structure (vertices and edges) - similar results from the literature required more involved encodings.
Cite as

Rémi Di Guardia, Olivier Laurent, Lorenzo Tortora de Falco, and Lionel Vaux Auclair. Yeo’s Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{diguardia_et_al:LIPIcs.FSCD.2025.16,
  author =	{Di Guardia, R\'{e}mi and Laurent, Olivier and Tortora de Falco, Lorenzo and Vaux Auclair, Lionel},
  title =	{{Yeo’s Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{16:1--16:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.16},
  URN =		{urn:nbn:de:0030-drops-236317},
  doi =		{10.4230/LIPIcs.FSCD.2025.16},
  annote =	{Keywords: Linear Logic, Proof Net, Sequentialization, Graph Theory, Yeo’s Theorem}
}
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}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2016.25
Focusing in Orthologic

Authors: Olivier Laurent

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Abstract
We propose new sequent calculus systems for orthologic (also known as minimal quantum logic) which satisfy the cut elimination property. The first one is a very simple system relying on the involutive status of negation. The second one incorporates the notion of focusing (coming from linear logic) to add constraints on proofs and thus to facilitate proof search. We demonstrate how to take benefits from the new systems in automatic proof search for orthologic.
Cite as

Olivier Laurent. Focusing in Orthologic. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 25:1-25:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{laurent:LIPIcs.FSCD.2016.25,
  author =	{Laurent, Olivier},
  title =	{{Focusing in Orthologic}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{25:1--25:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.25},
  URN =		{urn:nbn:de:0030-drops-59805},
  doi =		{10.4230/LIPIcs.FSCD.2016.25},
  annote =	{Keywords: orthologic, focusing, minimal quantum logic, linear logic, automatic proof search, cut elimination}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact