Search Results

Documents authored by Vemclefs, Maxime

Artifact
Software
DOI: 10.4230/artifacts.23906
adrilancelot/Abella-lambda-Barendregt-theory

Authors: Adrienne Lancelot, Beniamino Accattoli, and Maxime Vemclefs

Abstract
Cite as

Adrienne Lancelot, Beniamino Accattoli, Maxime Vemclefs. adrilancelot/Abella-lambda-Barendregt-theory (Software, Abella formalization code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{AbellaSources,
   title = {{adrilancelot/Abella-lambda-Barendregt-theory}}, 
   author = {Lancelot, Adrienne and Accattoli, Beniamino and Vemclefs, Maxime},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:b20ffd2d8d946adac1eb2fffa72112d23a2deeed;origin=https://github.com/adrilancelot/Abella-lambda-Barendregt-theory;visit=swh:1:snp:51adf802a55fe82840e4e8d940b31babccdb58a2;anchor=swh:1:rev:07ea3f03983145ce1b7e070e3afbe9ff730d2531}{\texttt{swh:1:dir:b20ffd2d8d946adac1eb2fffa72112d23a2deeed}} (visited on 2025-09-22)},
   url = {https://github.com/adrilancelot/Abella-lambda-Barendregt-theory},
   doi = {10.4230/artifacts.23906},
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.13
Barendregt’s Theory of the λ-Calculus, Refreshed and Formalized

Authors: Adrienne Lancelot, Beniamino Accattoli, and Maxime Vemclefs

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Barendregt’s book on the untyped λ-calculus refines the inconsistent view of β-divergence as representation of the undefined via the key concept of head reduction. In this paper, we put together recent revisitations of some key theorems laid out in Barendregt’s book, and we formalize them in the Abella proof assistant. Our work provides a compact and refreshed presentation of the core of the book. The formalization faithfully mimics pen-and-paper proofs. Two interesting aspects are the manipulation of contexts for the study of contextual equivalence and a formal alternative to the informal trick at work in Takahashi’s proof of the genericity lemma. As a by-product, we obtain an alternative definition of contextual equivalence that does not mention contexts.
Cite as

Adrienne Lancelot, Beniamino Accattoli, and Maxime Vemclefs. Barendregt’s Theory of the λ-Calculus, Refreshed and Formalized. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 13:1-13:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lancelot_et_al:LIPIcs.ITP.2025.13,
  author =	{Lancelot, Adrienne and Accattoli, Beniamino and Vemclefs, Maxime},
  title =	{{Barendregt’s Theory of the \lambda-Calculus, Refreshed and Formalized}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{13:1--13:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.13},
  URN =		{urn:nbn:de:0030-drops-246114},
  doi =		{10.4230/LIPIcs.ITP.2025.13},
  annote =	{Keywords: lambda-calculus, head reduction, equational theory}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact