3 Search Results for "Jacobé de Naurois, Paulin"

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.CSL.2022.26
Parallelism in Soft Linear Logic

Authors: Paulin Jacobé de Naurois

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Abstract
We extend the Soft Linear Logic of Lafont with a new kind of modality, called parallel. Contractions on parallel modalities are only allowed in the cut and the left ⊸ rules, in a controlled, uniformly distributive way. We show that SLL, extended with this parallel modality, is sound and complete for PSPACE. We propose a corresponding typing discipline for the λ-calculus, extending the STA typing system of Gaboardi and Ronchi, and establish its PSPACE soundness and completeness. The use of the parallel modality in the cut-rule drives a polynomial-time, parallel call-by-value evaluation strategy of the terms.
Cite as

Paulin Jacobé de Naurois. Parallelism in Soft Linear Logic. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 26:1-26:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{jacobedenaurois:LIPIcs.CSL.2022.26,
  author =	{Jacob\'{e} de Naurois, Paulin},
  title =	{{Parallelism in Soft Linear Logic}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{26:1--26:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.26},
  URN =		{urn:nbn:de:0030-drops-157468},
  doi =		{10.4230/LIPIcs.CSL.2022.26},
  annote =	{Keywords: Implicit Complexity, Typing, Linear Logic, Functional Programming}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.29
Pointers in Recursion: Exploring the Tropics

Authors: Paulin Jacobé de Naurois

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
We translate the usual class of partial/primitive recursive functions to a pointer recursion framework, accessing actual input values via a pointer reading unit-cost function. These pointer recursive functions classes are proven equivalent to the usual partial/primitive recursive functions. Complexity-wise, this framework captures in a streamlined way most of the relevant sub-polynomial classes. Pointer recursion with the safe/normal tiering discipline of Bellantoni and Cook corresponds to polylogtime computation. We introduce a new, non-size increasing tiering discipline, called tropical tiering. Tropical tiering and pointer recursion, used with some of the most common recursion schemes, capture the classes logspace, logspace/polylogtime, ptime, and NC. Finally, in a fashion reminiscent of the safe recursive functions, tropical tiering is expressed directly in the syntax of the function algebras, yielding the tropical recursive function algebras.
Cite as

Paulin Jacobé de Naurois. Pointers in Recursion: Exploring the Tropics. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{jacobedenaurois:LIPIcs.FSCD.2019.29,
  author =	{Jacob\'{e} de Naurois, Paulin},
  title =	{{Pointers in Recursion: Exploring the Tropics}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{29:1--29:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.29},
  URN =		{urn:nbn:de:0030-drops-105360},
  doi =		{10.4230/LIPIcs.FSCD.2019.29},
  annote =	{Keywords: Implicit Complexity, Recursion Theory}
}
  • Refine by Type
  • 3 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2022
  • 1 2019

  • Refine by Author
  • 2 Jacobé de Naurois, Paulin
  • 1 Di Guardia, Rémi
  • 1 Laurent, Olivier
  • 1 Tortora de Falco, Lorenzo
  • 1 Vaux Auclair, Lionel

  • Refine by Series/Journal
  • 3 LIPIcs

  • Refine by Classification
  • 2 Theory of computation → Complexity theory and logic
  • 2 Theory of computation → Linear logic
  • 1 Mathematics of computing → Graph coloring
  • 1 Software and its engineering → Recursion
  • 1 Theory of computation → Complexity classes

  • Refine by Keyword
  • 2 Implicit Complexity
  • 2 Linear Logic
  • 1 Functional Programming
  • 1 Graph Theory
  • 1 Proof Net
  • Show More...

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