2 Search Results for "Alcolei, Aurore"

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.CSL.2018.5

The True Concurrency of Herbrand's Theorem

Authors: Aurore Alcolei, Pierre Clairambault, Martin Hyland, and Glynn Winskel

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

Abstract

Herbrand's theorem, widely regarded as a cornerstone of proof theory, exposes some of the constructive content of classical logic. In its simplest form, it reduces the validity of a first-order purely existential formula to that of a finite disjunction. In the general case, it reduces first-order validity to propositional validity, by understanding the structure of the assignment of first-order terms to existential quantifiers, and the causal dependency between quantifiers. In this paper, we show that Herbrand's theorem in its general form can be elegantly stated and proved as a theorem in the framework of concurrent games, a denotational semantics designed to faithfully represent causality and independence in concurrent systems, thereby exposing the concurrency underlying the computational content of classical proofs. The causal structure of concurrent strategies, paired with annotations by first-order terms, is used to specify the dependency between quantifiers implicit in proofs. Furthermore concurrent strategies can be composed, yielding a compositional proof of Herbrand's theorem, simply by interpreting classical sequent proofs in a well-chosen denotational model.

Cite as

Aurore Alcolei, Pierre Clairambault, Martin Hyland, and Glynn Winskel. The True Concurrency of Herbrand's Theorem. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{alcolei_et_al:LIPIcs.CSL.2018.5,
  author =	{Alcolei, Aurore and Clairambault, Pierre and Hyland, Martin and Winskel, Glynn},
  title =	{{The True Concurrency of Herbrand's Theorem}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{5:1--5:22},
  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.5},
  URN =		{urn:nbn:de:0030-drops-96723},
  doi =		{10.4230/LIPIcs.CSL.2018.5},
  annote =	{Keywords: Herbrand's theorem, Game semantics, True concurrency}
}

Refine by Type
2 Document/PDF

Refine by Publication Year
1 2026
1 2018

Refine by Author
1 Alcolei, Aurore
1 Castellan, Simon
1 Clairambault, Pierre
1 Hyland, Martin
1 Paquet, Hugo
Show More...

Refine by Series/Journal
2 LIPIcs

Refine by Classification
2 Theory of computation → Denotational semantics
1 Theory of computation → Categorical semantics
1 Theory of computation → Probabilistic computation
1 Theory of computation → Proof theory

Refine by Keyword
1 Categorical semantics
1 Game semantics
1 Herbrand's theorem
1 True concurrency
1 interpreter
Show More...

2 Search Results for "Alcolei, Aurore"

Lazy Intermediate Representations for Algebraic Effects

Abstract

Cite as

The True Concurrency of Herbrand's Theorem

Abstract

Cite as

Thanks for your feedback!

Could not send message