Search Results

Documents authored by Laurent, Olivier

Artifact
Software
DOI: 10.4230/artifacts.26938
Intersection Subtyping with Fixpoints

Authors: Olivier Laurent and Jui-Hsuan Wu

Abstract
Cite as

Olivier Laurent, Jui-Hsuan Wu. Intersection Subtyping with Fixpoints (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-26938,
   title = {{Intersection Subtyping with Fixpoints}}, 
   author = {Laurent, Olivier and Wu, Jui-Hsuan},
   note = {Software, ANR-21-CE48-0019, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:c8749a7a0cf20e8d37b276595ce0183002fba666;origin=https://github.com/olaure01/islogic;visit=swh:1:snp:d08507fa4c74499420710f1243109b57ad0a4a6d;anchor=swh:1:rev:f0a7d29f8b6c6d3b43d6abb578a6502892600b0e}{\texttt{swh:1:dir:c8749a7a0cf20e8d37b276595ce0183002fba666}} (visited on 2026-07-15)},
   url = {https://github.com/olaure01/islogic/tree/FSCD2026},
   doi = {10.4230/artifacts.26938},
}
Document
DOI: 10.4230/LIPIcs.FSCD.2026.22
Non-Wellfounded Derivations for Intersection Subtyping with Fixpoints

Authors: Olivier Laurent and Jui-Hsuan Wu

Published in: LIPIcs, Volume 378, 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)

Abstract
Subtyping is a key ingredient of many intersection type systems. In the case of the BCD system, B. Pierce gave a transitivity-free presentation of subtyping. This provides better structural properties for the analysis of this relation and leads to a simple decision algorithm. We generalize this transitivity-free approach to a general class of extensions of BCD allowing to impose some pre-order as well as some fixpoint equations on atoms. This includes in particular the case of various intersection type systems compatible with η-equality (Scott, Park, etc.). Proving the equivalence between the transitivity-free systems and their BCD-style presentation is addressed by means of cut-elimination techniques from proof theory. Due to the presence of fixpoints, we are led to introduce non-wellfounded derivations. In the context of the structural analysis of intersection subtyping, this happens to be the first use of infinitary derivations.
Cite as

Olivier Laurent and Jui-Hsuan Wu. Non-Wellfounded Derivations for Intersection Subtyping with Fixpoints. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 22:1-22:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{laurent_et_al:LIPIcs.FSCD.2026.22,
  author =	{Laurent, Olivier and Wu, Jui-Hsuan},
  title =	{{Non-Wellfounded Derivations for Intersection Subtyping with Fixpoints}},
  booktitle =	{11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
  pages =	{22:1--22:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-433-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{378},
  editor =	{Pfenning, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.22},
  URN =		{urn:nbn:de:0030-drops-263721},
  doi =		{10.4230/LIPIcs.FSCD.2026.22},
  annote =	{Keywords: Intersection types, subtyping, non-wellfounded proofs, fixpoints, cut elimination}
}
Artifact
Software
DOI: 10.4230/artifacts.26957
IS Logic

Authors: Olivier Laurent

Abstract
Cite as

Olivier Laurent. IS Logic (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-26957,
   title = {{IS Logic}}, 
   author = {Laurent, Olivier},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:682600883bd8fd60057d332c6a87a39c047f22e7;origin=https://github.com/olaure01/islogic;visit=swh:1:snp:008009b1529ca9e9da568c9be43b0e91b90ebbd2;anchor=swh:1:rev:e2cfc80de9876c8515ecb347038ae617a108c73c}{\texttt{swh:1:dir:682600883bd8fd60057d332c6a87a39c047f22e7}} (visited on 2026-07-09)},
   url = {https://github.com/olaure01/islogic/tree/LICS2026},
   doi = {10.4230/artifacts.26957},
}
Document
DOI: 10.4230/LIPIcs.LICS.2026.62
The Logic of Intersection Subtyping

Authors: Olivier Laurent

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract
The subtyping relation of programming languages can be analysed as an entailment relation by means of proof theory. We are interested in two main families of systems: intersection types and polymorphic subtyping. They share the fact that implication has some distributivity property: over intersection in the first case and over universal quantification in the second one. We introduce a restriction of the second-order (full) Lambek calculus which is stable under cut-elimination and conservatively extends these two subtyping relations. This new system IS is an intuitionistic non-commutative linear sequent calculus which provides a natural logical setting for the study of subtyping relations. We recover sequent calculi from the literature (as well as new variants) as restrictions of IS (thanks to the proof-theoretical analysis of the system: admissible rules, invertibility, focusing, etc.), so that IS appears as a unifying logic for subtyping. We also develop translations relating IS with relevant logic, the (unconstrained) Lambek calculus or cyclic linear logic.
Cite as

Olivier Laurent. The Logic of Intersection Subtyping. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 62:1-62:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{laurent:LIPIcs.LICS.2026.62,
  author =	{Laurent, Olivier},
  title =	{{The Logic of Intersection Subtyping}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{62:1--62:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.62},
  URN =		{urn:nbn:de:0030-drops-268497},
  doi =		{10.4230/LIPIcs.LICS.2026.62},
  annote =	{Keywords: Intersection types, subtyping, polymorphic subtyping, Lambek calculus, linear logic, cut elimination}
}
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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact