4 Search Results for "Hughes, Dominic J. D."

Document
DOI: 10.4230/LIPIcs.CSL.2026.12
String Diagrams for Closed Symmetric Monoidal Categories

Authors: Callum Reader and Alessandro Di Giorgio

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
We introduce a graphical language for closed symmetric monoidal categories based on an extension of string diagrams with special bracket wires representing internal homs. These bracket wires make the structure of the internal hom functor explicit, allowing standard morphism wires to interact with them through a well-defined set of graphical rules. We establish the soundness and completeness of the diagrammatic calculus, and illustrate its expressiveness through examples drawn from category theory, logic and programming language semantics.
Cite as

Callum Reader and Alessandro Di Giorgio. String Diagrams for Closed Symmetric Monoidal Categories. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{reader_et_al:LIPIcs.CSL.2026.12,
  author =	{Reader, Callum and Di Giorgio, Alessandro},
  title =	{{String Diagrams for Closed Symmetric Monoidal Categories}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{12:1--12:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.12},
  URN =		{urn:nbn:de:0030-drops-254369},
  doi =		{10.4230/LIPIcs.CSL.2026.12},
  annote =	{Keywords: diagrammatic languages, logic, lambda calculi}
}
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.2022.19
Normalization Without Syntax

Authors: Willem B. Heijltjes, Dominic J. D. Hughes, and Lutz Straßburger

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
We present normalization for intuitionistic combinatorial proofs (ICPs) and relate it to the simply-typed lambda-calculus. We prove confluence and strong normalization. Combinatorial proofs, or "proofs without syntax", form a graphical semantics of proof in various logics that is canonical yet complexity-aware: they are a polynomial-sized representation of sequent proofs that factors out exactly the non-duplicating permutations. Our approach to normalization aligns with these characteristics: it is canonical (free of permutations) and generic (readily applied to other logics). Our reduction mechanism is a canonical representation of reduction in sequent calculus with closed cuts (no abstraction is allowed below a cut), and relates to closed reduction in lambda-calculus and supercombinators. While we will use ICPs concretely, the notion of reduction is completely abstract, and can be specialized to give a reduction mechanism for any representation of typed normal forms.
Cite as

Willem B. Heijltjes, Dominic J. D. Hughes, and Lutz Straßburger. Normalization Without Syntax. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{heijltjes_et_al:LIPIcs.FSCD.2022.19,
  author =	{Heijltjes, Willem B. and Hughes, Dominic J. D. and Stra{\ss}burger, Lutz},
  title =	{{Normalization Without Syntax}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{19:1--19:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.19},
  URN =		{urn:nbn:de:0030-drops-163004},
  doi =		{10.4230/LIPIcs.FSCD.2022.19},
  annote =	{Keywords: combinatorial proofs, intuitionistic logic, lambda-calculus, Curry-Howard, proof nets}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.22
Proof Nets for First-Order Additive Linear Logic

Authors: Willem B. Heijltjes, Dominic J. D. Hughes, and Lutz Straßburger

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

Abstract
We present canonical proof nets for first-order additive linear logic, the fragment of linear logic with sum, product, and first-order universal and existential quantification. We present two versions of our proof nets. One, witness nets, retains explicit witnessing information to existential quantification. For the other, unification nets, this information is absent but can be reconstructed through unification. Unification nets embody a central contribution of the paper: first-order witness information can be left implicit, and reconstructed as needed. Witness nets are canonical for first-order additive sequent calculus. Unification nets in addition factor out any inessential choice for existential witnesses. Both notions of proof net are defined through coalescence, an additive counterpart to multiplicative contractibility, and for witness nets an additional geometric correctness criterion is provided. Both capture sequent calculus cut-elimination as a one-step global composition operation.
Cite as

Willem B. Heijltjes, Dominic J. D. Hughes, and Lutz Straßburger. Proof Nets for First-Order Additive Linear Logic. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 22:1-22:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{heijltjes_et_al:LIPIcs.FSCD.2019.22,
  author =	{Heijltjes, Willem B. and Hughes, Dominic J. D. and Stra{\ss}burger, Lutz},
  title =	{{Proof Nets for First-Order Additive Linear Logic}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{22:1--22:22},
  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.22},
  URN =		{urn:nbn:de:0030-drops-105297},
  doi =		{10.4230/LIPIcs.FSCD.2019.22},
  annote =	{Keywords: linear logic, first-order logic, proof nets, Herbrand’s theorem}
}
  • Refine by Type
  • 4 Document/PDF
  • 2 Document/HTML

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

  • Refine by Author
  • 2 Heijltjes, Willem B.
  • 2 Hughes, Dominic J. D.
  • 2 Straßburger, Lutz
  • 1 Di Giorgio, Alessandro
  • 1 Di Guardia, Rémi
  • Show More...

  • Refine by Series/Journal
  • 4 LIPIcs

  • Refine by Classification
  • 2 Theory of computation → Linear logic
  • 2 Theory of computation → Proof theory
  • 1 Mathematics of computing → Graph coloring
  • 1 Theory of computation → Categorical semantics
  • 1 Theory of computation → Lambda calculus
  • Show More...

  • Refine by Keyword
  • 2 proof nets
  • 1 Curry-Howard
  • 1 Graph Theory
  • 1 Herbrand’s theorem
  • 1 Linear Logic
  • 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