DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2026.11

Approximation Theory for Distant Bang Calculus

Authors: Kostia Chardonnet, Jules Chouquet, and Axel Kerinec

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

Abstract

Approximation semantics capture the observable behaviour of λ-terms. Böhm Trees and Taylor Expansion are its two central paradigms, related by the Commutation Theorem. While these notions are well understood in Call-by-Name (CbN), they have only recently been developed for Call-by-Value (CbV), which motivate the search for a unified approximation framework. The Bang-calculus provides such a framework: it subsumes both CbN and CbV through linear-logic translations and enjoys robust rewriting properties. We develop the approximation semantics of dBang (the Bang-calculus with explicit substitutions and distant reductions) by introducing approximation trees in the Böhm tradition together with Taylor expansion. We establish their fundamental properties, including a commutation theorem. Via translations, our results recover the CbN and CbV cases within a single unifying framework capturing infinitary and resource-sensitive semantics.

Cite as

Kostia Chardonnet, Jules Chouquet, and Axel Kerinec. Approximation Theory for Distant Bang Calculus. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{chardonnet_et_al:LIPIcs.FSCD.2026.11,
  author =	{Chardonnet, Kostia and Chouquet, Jules and Kerinec, Axel},
  title =	{{Approximation Theory for Distant Bang Calculus}},
  booktitle =	{11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
  pages =	{11:1--11: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.11},
  URN =		{urn:nbn:de:0030-drops-263612},
  doi =		{10.4230/LIPIcs.FSCD.2026.11},
  annote =	{Keywords: Lambda-calculus, B\"{o}hm Trees, Taylor expansion of lambda-terms}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2021.7

Call-By-Value, Again!

Authors: Axel Kerinec, Giulio Manzonetto, and Simona Ronchi Della Rocca

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract

The quest for a fully abstract model of the call-by-value λ-calculus remains crucial in programming language theory, and constitutes an ongoing line of research. While a model enjoying this property has not been found yet, this interesting problem acts as a powerful motivation for investigating classes of models, studying the associated theories and capturing operational properties semantically. We study a relational model presented as a relevant intersection type system, where intersection is in general non-idempotent, except for an idempotent element that is injected in the system. This model is adequate, equates many λ-terms that are indeed equivalent in the maximal observational theory, and satisfies an Approximation Theorem w.r.t. a system of approximants representing finite pieces of call-by-value Böhm trees. We show that these tools can be used for characterizing the most significant properties of the calculus - namely valuability, potential valuability and solvability - both semantically, through the notion of approximants, and logically, by means of the type assignment system. We mainly focus on the characterizations of solvability, as they constitute an original result. Finally, we prove the decidability of the inhabitation problem for our type system by exhibiting a non-deterministic algorithm, which is proven sound, correct and terminating.

Cite as

Axel Kerinec, Giulio Manzonetto, and Simona Ronchi Della Rocca. Call-By-Value, Again!. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{kerinec_et_al:LIPIcs.FSCD.2021.7,
  author =	{Kerinec, Axel and Manzonetto, Giulio and Ronchi Della Rocca, Simona},
  title =	{{Call-By-Value, Again!}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{7:1--7:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.7},
  URN =		{urn:nbn:de:0030-drops-142458},
  doi =		{10.4230/LIPIcs.FSCD.2021.7},
  annote =	{Keywords: \lambda-calculus, call-by-value, intersection types, solvability, inhabitation}
}

Search Results

Documents authored by Kerinec, Axel

Approximation Theory for Distant Bang Calculus

Abstract

Cite as

Call-By-Value, Again!

Abstract

Cite as

Thanks for your feedback!

Could not send message