Search Results

Documents authored by Paquet, Hugo

Document
DOI: 10.4230/LIPIcs.FSCD.2026.23
Universal Properties of Petri Net Unfoldings

Authors: Serge Lechenne and Hugo Paquet

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

Abstract
It is an established idea in concurrency theory that every Petri net admits an unfolding semantics. This is a denotational object that represents its domain of possible executions. Unfoldings play an important role in practical analysis and verification. This paper is concerned with the following well-known problem: while the unfolding resembles a universal construction in the category of Petri nets, it generally fails to satisfy the expected universal property. This is because the unfolding construction overlooks the net’s internal symmetries. There are two solutions: make these symmetries explicit to obtain a weak universal property (one that holds only "up to symmetry"); or break the symmetries by assigning individual identities to components of the net. We review these two solutions and establish, in each case, a universal unfolding of Petri nets to event structures. This paper demonstrates a 2-categorical approach to Petri net unfoldings. We show that each unfolding semantics determines a 2-categorical relative adjunction involving Petri nets and event structures. Viewed in this way, the above two constructions can be related formally via an appropriate morphism of adjunctions. We exhibit a 2-density property of event structures which implies that unfolding functors are essentially unique.
Cite as

Serge Lechenne and Hugo Paquet. Universal Properties of Petri Net Unfoldings. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 23:1-23:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{lechenne_et_al:LIPIcs.FSCD.2026.23,
  author =	{Lechenne, Serge and Paquet, Hugo},
  title =	{{Universal Properties of Petri Net Unfoldings}},
  booktitle =	{11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
  pages =	{23:1--23:19},
  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.23},
  URN =		{urn:nbn:de:0030-drops-263734},
  doi =		{10.4230/LIPIcs.FSCD.2026.23},
  annote =	{Keywords: Petri nets, Event structures, Symmetry, Unfolding, 2-Categories}
}
Document
DOI: 10.4230/LIPIcs.LICS.2026.25
Lazy Intermediate Representations for Algebraic Effects

Authors: Simon Castellan and Hugo Paquet

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

Abstract
A lazy program interpreter postpones computation until the result is actually needed. This is typically more efficient than an eager (or call-by-value) interpreter, but a concern is that the semantics is not generally preserved. We propose a new semantic analysis of lazy evaluation that relies on a subtle combination of name generation and read-only state. Our perspective is that laziness arises from a hybrid evaluation strategy, in which only the name generation follows call-by-value. This semantic model suggests better intermediate representations of sum and product types in a lazy interpreter, along with equations that justify further optimizations. We illustrate this with an implementation in OCaml. Our motivation is practical: the origin of this work is a real-world application of discrete probabilistic programming, in which large algebraic data types cause significant performance issues with a call-by-value interpreter. Our lazy semantics justifies better optimized representations, and provides principled foundations for other methods involving laziness in probabilistic programming.
Cite as

Simon Castellan and Hugo Paquet. Lazy Intermediate Representations for Algebraic Effects. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 25:1-25:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{castellan_et_al:LIPIcs.LICS.2026.25,
  author =	{Castellan, Simon and Paquet, Hugo},
  title =	{{Lazy Intermediate Representations for Algebraic Effects}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{25:1--25:27},
  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.25},
  URN =		{urn:nbn:de:0030-drops-268124},
  doi =		{10.4230/LIPIcs.LICS.2026.25},
  annote =	{Keywords: Categorical semantics, lazy evaluation, interpreter, probabilistic programming}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.10
Categorical Continuation Semantics for Concurrency

Authors: Flavien Breuvart and Hugo Paquet

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

Abstract
Continuation semantics for simple programming languages can be axiomatized as a dialogue category: a symmetric monoidal category equipped with a negation operation. This axiomatization makes clear the relationship between game semantics, CPS transformations, and continuation monads. In this paper we extend dialogue categories with 2-categorical structure and concurrent primitives. This is inspired by a recent analysis of concurrency based on 2-categorical monads. We show that the fine-grained structure of dialogue categories, not generally available in other semantic models, can be exploited to give a type to concurrent primitives join and fork. Our main theorem is that this simple axiomatization induces a concurrent continuation 2-monad. We also show that this framework is expressive beyond call-by-value monadic programming. The definitions in this paper are illustrated by concrete constructions in concurrent game semantics, and our results give a formal categorical basis for concurrent strategies. From a more practical perspective, our approach suggests a candidate target language for linear CPS transformations of concurrent programming languages.
Cite as

Flavien Breuvart and Hugo Paquet. Categorical Continuation Semantics for Concurrency. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 10:1-10:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{breuvart_et_al:LIPIcs.FSCD.2025.10,
  author =	{Breuvart, Flavien and Paquet, Hugo},
  title =	{{Categorical Continuation Semantics for Concurrency}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{10:1--10:21},
  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.10},
  URN =		{urn:nbn:de:0030-drops-236251},
  doi =		{10.4230/LIPIcs.FSCD.2025.10},
  annote =	{Keywords: denotational semantics, 2-categories, concurrency, continuations, game semantics}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2022.31
A Combinatorial Approach to Higher-Order Structure for Polynomial Functors

Authors: Marcelo Fiore, Zeinab Galal, and Hugo Paquet

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

Abstract
Polynomial functors are categorical structures used in a variety of applications across theoretical computer science; for instance, in database theory, denotational semantics, functional programming, and type theory. A well-known problem is that the bicategory of finitary polynomial functors between categories of indexed sets is not cartesian closed, despite its success and influence on denotational models and linear logic. This paper introduces a formal bridge between the model of finitary polynomial functors and the combinatorial theory of generalised species of structures. Our approach consists in viewing finitary polynomial functors as free analytic functors, which correspond to free generalised species. In order to systematically consider finitary polynomial functors from this combinatorial perspective, we study a model of groupoids with additional logical structure; this is used to constrain the generalised species between them. The result is a new cartesian closed bicategory that embeds finitary polynomial functors.
Cite as

Marcelo Fiore, Zeinab Galal, and Hugo Paquet. A Combinatorial Approach to Higher-Order Structure for Polynomial Functors. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{fiore_et_al:LIPIcs.FSCD.2022.31,
  author =	{Fiore, Marcelo and Galal, Zeinab and Paquet, Hugo},
  title =	{{A Combinatorial Approach to Higher-Order Structure for Polynomial Functors}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{31:1--31: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.31},
  URN =		{urn:nbn:de:0030-drops-163129},
  doi =		{10.4230/LIPIcs.FSCD.2022.31},
  annote =	{Keywords: Bicategorical models, denotational semantics, stable domain theory, linear logic, polynomial functors, species of structures, groupoids}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.16
Fully Abstract Models of the Probabilistic lambda-calculus

Authors: Pierre Clairambault and Hugo Paquet

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
We compare three models of the probabilistic lambda-calculus: the probabilistic Böhm trees of Leventis, the probabilistic concurrent games of Winskel et al., and the weighted relational model of Ehrhard et al. Probabilistic Böhm trees and probabilistic strategies are shown to be related by a precise correspondence theorem, in the spirit of existing work for the pure lambda-calculus. Using Leventis' theorem (probabilistic Böhm trees characterise observational equivalence), we derive a full abstraction result for the games model. Then, we relate probabilistic strategies to the weighted relational model, using an interpretation-preserving functor from the former to the latter. We obtain that the relational model is also fully abstract.
Cite as

Pierre Clairambault and Hugo Paquet. Fully Abstract Models of the Probabilistic lambda-calculus. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{clairambault_et_al:LIPIcs.CSL.2018.16,
  author =	{Clairambault, Pierre and Paquet, Hugo},
  title =	{{Fully Abstract Models of the Probabilistic lambda-calculus}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{16:1--16:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.16},
  URN =		{urn:nbn:de:0030-drops-96835},
  doi =		{10.4230/LIPIcs.CSL.2018.16},
  annote =	{Keywords: Game Semantics, Lambda-calculus, Probabilistic programming, Relational model, Full abstraction}
}
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