Document Open Access Logo

Barendregt’s Theory of the λ-Calculus, Refreshed and Formalized

Authors Adrienne Lancelot , Beniamino Accattoli , Maxime Vemclefs

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.ITP.2025.13.pdf
  • Filesize: 0.89 MB
  • 22 pages
HTML5 Logo HTML (experimental)
LIPIcs.ITP.2025.13.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
Keywords
  • lambda-calculus
  • head reduction
  • equational theory

Metrics

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.ITP.2025.13

Author Details

Adrienne Lancelot
  • Inria & LIX, Ecole Polytechnique, UMR 7161, Paris, France
  • Université Paris Cité, CNRS, IRIF, F-75013, Paris, France
Beniamino Accattoli
  • Inria & LIX, Ecole Polytechnique, UMR 7161, Paris, France
Maxime Vemclefs
  • Independent, Paris, France

Supplementary Materials

References

  1. Andreas Abel. Abella proof of the standardization theorem for the lambda calculus, 2009. URL: https://abella-prover.org/examples/lambda-calculus/sred.html.
  2. Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer, and Kathrin Stark. POPLMark reloaded: Mechanizing proofs by logical relations. Journal of Functional Programming, 29:e19, 2019. URL: https://doi.org/10.1017/S0956796819000170.
  3. Abella. Reference guide. URL: https://abella-prover.org/reference-guide.html.
  4. Beniamino Accattoli. Proof pearl: Abella formalization of λ-calculus cube property. In Chris Hawblitzel and Dale Miller, editors, Certified Programs and Proofs - Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings, volume 7679 of Lecture Notes in Computer Science, pages 173-187. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-35308-6_15.
  5. Beniamino Accattoli, Horace Blanc, and Claudio Sacerdoti Coen. Formalizing functions as processes. In Adam Naumowicz and René Thiemann, editors, 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Bialystok, Poland, volume 268 of LIPIcs, pages 5:1-5:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.ITP.2023.5.
  6. Beniamino Accattoli, Eduardo Bonelli, Delia Kesner, and Carlos Lombardi. A nonstandard standardization theorem. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 659-670. ACM, 2014. URL: https://doi.org/10.1145/2535838.2535886.
  7. Beniamino Accattoli and Ugo Dal Lago. On the invariance of the unitary cost model for head reduction. In Ashish Tiwari, editor, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) , RTA 2012, May 28 - June 2, 2012, Nagoya, Japan, volume 15 of LIPIcs, pages 22-37. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPICS.RTA.2012.22.
  8. Beniamino Accattoli, Claudia Faggian, and Giulio Guerrieri. Factorization and normalization, essentially. In Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, pages 159-180, 2019. URL: https://doi.org/10.1007/978-3-030-34175-6_9.
  9. Beniamino Accattoli and Adrienne Lancelot. Light genericity. In Naoki Kobayashi and James Worrell, editors, Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part II, volume 14575 of Lecture Notes in Computer Science, pages 24-46. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57231-9_2.
  10. Victor Arrial, Giulio Guerrieri, and Delia Kesner. Genericity through stratification. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '24, New York, NY, USA, 2024. Association for Computing Machinery. URL: https://doi.org/10.1145/3661814.3662113.
  11. Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized metatheory for the masses: The POPLMark challenge. In Joe Hurd and Thomas F. Melham, editors, Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, volume 3603 of Lecture Notes in Computer Science, pages 50-65. Springer, 2005. URL: https://doi.org/10.1007/11541868_4.
  12. David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, and Yuting Wang. Abella: A system for reasoning about relational specifications. J. Formaliz. Reason., 7(2):1-89, 2014. URL: https://doi.org/10.6092/ISSN.1972-5787/4650.
  13. Davide Barbarossa and Giulio Manzonetto. Taylor subsumes Scott, Berry, Kahn and Plotkin. Proc. ACM Program. Lang., 4(POPL):1:1-1:23, 2020. URL: https://doi.org/10.1145/3371069.
  14. Hendrik Pieter Barendregt. Some extensional term models for combinatory logics and λ-calculi. PhD thesis, Univ. Utrecht, 1971. Google Scholar
  15. Hendrik Pieter Barendregt. The Lambda Calculus - Its Syntax and Semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1984. Google Scholar
  16. Henk Barendregt. Representing 'undefined' in lambda calculus. J. Funct. Program., 2(3):367-374, 1992. URL: https://doi.org/10.1017/S0956796800000447.
  17. Henk Barendregt and Giulio Manzonetto. A Lambda Calculus Satellite. College Publications, 2022. URL: https://www.collegepublications.co.uk/logic/mlf/?00035.
  18. Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. Proving soundness of extensional normal-form bisimilarities. Electronic Notes in Theoretical Computer Science, 336:41-56, 2018. The Thirty-third Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIII). URL: https://doi.org/10.1016/j.entcs.2018.03.015.
  19. Douglas Bridges and Fred Richman. Varieties of Constructive Mathematics. London Mathematical Society Lecture Note Series. Cambridge University Press, 1987. URL: https://doi.org/10.1017/CBO9780511565663.
  20. Marco Carbone, David Castro-Perez, Francisco Ferreira, Lorenzo Gheri, Frederik Krogsdal Jacobsen, Alberto Momigliano, Luca Padovani, Alceste Scalas, Dawit Legesse Tirore, Martin Vassor, Nobuko Yoshida, and Daniel Zackon. The concurrent calculi formalisation benchmark. In Ilaria Castellani and Francesco Tiezzi, editors, Coordination Models and Languages - 26th IFIP WG 6.1 International Conference, COORDINATION 2024, Held as Part of the 19th International Federated Conference on Distributed Computing Techniques, DisCoTec 2024, Groningen, The Netherlands, June 17-21, 2024, Proceedings, volume 14676 of Lecture Notes in Computer Science, pages 149-158. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-62697-5_9.
  21. Kaustuv Chaudhuri, Matteo Cimini, and Dale Miller. A lightweight formalization of the metatheory of bisimulation-up-to. In Xavier Leroy and Alwen Tiu, editors, Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pages 157-166. ACM, 2015. URL: https://doi.org/10.1145/2676724.2693170.
  22. Karl Crary. A simple proof of call-by-value standardization. Technical Report CMU-CS-09-137, Carnegie Mellon University, 2009. Google Scholar
  23. Ugo Dal Lago and Simone Martini. The weak lambda calculus as a reasonable machine. Theor. Comput. Sci., 398(1-3):32-50, 2008. URL: https://doi.org/10.1016/J.TCS.2008.01.044.
  24. Lavinia Egidi, Furio Honsell, and Simona Ronchi Della Rocca. Operational, denotational and logical descriptions: a case study. Fundam. Informaticae, 16(1):149-169, 1992. URL: https://doi.org/10.3233/FI-1992-16205.
  25. Jörg Endrullis and Roel C. de Vrijer. Reduction under substitution. In Andrei Voronkov, editor, Rewriting Techniques and Applications, 19th International Conference, RTA 2008, Hagenberg, Austria, July 15-17, 2008, Proceedings, volume 5117 of Lecture Notes in Computer Science, pages 425-440. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-70590-1_29.
  26. Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar. On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control. Proc. ACM Program. Lang., 1(ICFP), August 2017. URL: https://doi.org/10.1145/3110257.
  27. Yannick Forster, Steven Schäfer, Simon Spies, and Kathrin Stark. Call-by-push-value in Coq: operational, equational, and denotational theory. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, pages 118-131, New York, NY, USA, 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3293880.3294097.
  28. Andrew Gacek. The Abella interactive theorem prover (system description). In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, volume 5195 of Lecture Notes in Computer Science, pages 154-161. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-71070-7_13.
  29. Andrew Gacek, Dale Miller, and Gopalan Nadathur. Nominal abstraction. Inf. Comput., 209(1):48-73, 2011. URL: https://doi.org/10.1016/J.IC.2010.09.004.
  30. Lorenzo Gheri and Andrei Popescu. Case Studies in Formal Reasoning About lambda-Calculus: Semantics, Church-Rosser, Standardization and HOAS. CoRR, abs/2107.11674, 2021. URL: https://arxiv.org/abs/2107.11674.
  31. Silvia Ghilezan. Full intersection types and topologies in lambda calculus. J. Comput. Syst. Sci., 62(1):1-14, 2001. URL: https://doi.org/10.1006/jcss.2000.1703.
  32. Georges Gonthier, Jean-Jacques Lévy, and Paul-André Melliès. An abstract standardisation theorem. In Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS '92), Santa Cruz, California, USA, June 22-25, 1992, pages 72-81. IEEE Computer Society, 1992. URL: https://doi.org/10.1109/LICS.1992.185521.
  33. Ferruccio Guidi. Standardization and confluence in pure lambda-calculus formalized for the Matita theorem prover. J. Formaliz. Reason., 5(1):1-25, 2012. URL: https://doi.org/10.6092/ISSN.1972-5787/3392.
  34. Peter V. Homeier. A proof of the Church-Rosser theorem for the λ-calculus in higher order logic. In TPHOLs’01: Supplemental Proceedings, pages 207-222, 2001. Google Scholar
  35. Gérard P. Huet. Residual theory in lambda-calculus: A formal development. J. Funct. Program., 4(3):371-394, 1994. URL: https://doi.org/10.1017/S0956796800001106.
  36. Jonas Kaiser, Brigitte Pientka, and Gert Smolka. Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga. In Dale Miller, editor, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), volume 84 of Leibniz International Proceedings in Informatics (LIPIcs), pages 21:1-21:19, Dagstuhl, Germany, 2017. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2017.21.
  37. Richard Kennaway, Vincent van Oostrom, and Fer-Jan de Vries. Meaningless terms in rewriting. J. Funct. Log. Program., 1999(1), 1999. URL: http://danae.uni-muenster.de/lehre/kuchen/JFLP/articles/1999/A99-01/A99-01.html.
  38. Jean-Louis Krivine. Lambda-calculus, types and models. Ellis Horwood series in computers and their applications. Masson, 1993. Google Scholar
  39. Jan Kuper. Proving the genericity lemma by leftmost reduction is simple. In Jieh Hsiang, editor, Rewriting Techniques and Applications, 6th International Conference, RTA-95, Kaiserslautern, Germany, April 5-7, 1995, Proceedings, volume 914 of Lecture Notes in Computer Science, pages 271-278. Springer, 1995. URL: https://doi.org/10.1007/3-540-59200-8_63.
  40. Adrienne Lancelot, Beniamino Accattoli, , and Maxime Vemclefs. adrilancelot/Abella-lambda-Barendregt-theory. Software, (visited on 2025-07-17). URL: https://github.com/adrilancelot/Abella-lambda-Barendregt-theory
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.23906
  41. Dominique Larchey-Wendling. A constructive mechanization of lambda calculus in Coq. Online comments and Coq formalization, 2017. URL: https://homepages.loria.fr/DLarchey/Lambda_Calculus/.
  42. Ralph Loader. Notes on simply typed lambda calculus. Technical report ECS-LFCS-98-381, University of Edinburgh, 1998. URL: https://www.lfcs.inf.ed.ac.uk/reports/98/ECS-LFCS-98-381/.
  43. James McKinna and Robert Pollack. Some lambda calculus and type theory formalized. J. Autom. Reasoning, 23(3-4):373-409, 1999. URL: https://doi.org/10.1023/A:1006294005493.
  44. Paul-André Melliès. Axiomatic rewriting theory I: A diagrammatic standardization theorem. In Aart Middeldorp, Vincent van Oostrom, Femke van Raamsdonk, and Roel C. de Vrijer, editors, Processes, Terms and Cycles: Steps on the Road to Infinity, Essays Dedicated to Jan Willem Klop, on the Occasion of His 60th Birthday, volume 3838 of Lecture Notes in Computer Science, pages 554-638. Springer, 2005. URL: https://doi.org/10.1007/11601548_23.
  45. Dale Miller and Gopalan Nadathur. Programming with Higher-Order Logic. Cambridge University Press, 2012. URL: http://www.cambridge.org/de/academic/subjects/computer-science/programming-languages-and-applied-logic/programming-higher-order-logic?format=HB.
  46. Dale Miller and Alwen Tiu. A proof theory for generic judgments. ACM Trans. Comput. Log., 6(4):749-783, 2005. URL: https://doi.org/10.1145/1094622.1094628.
  47. Alberto Momigliano. A supposedly fun thing I may have to do again: a HOAS encoding of Howe’s method. In Proceedings of the Seventh International Workshop on Logical Frameworks and Meta-Languages, Theory and Practice, LFMTP '12, pages 33-42, New York, NY, USA, 2012. Association for Computing Machinery. URL: https://doi.org/10.1145/2364406.2364411.
  48. Julian Nagele, Vincent van Oostrom, and Christian Sternagel. A short mechanized proof of the Church-Rosser theorem by the Z-property for the λβ-calculus in Nominal Isabelle. CoRR, abs/1609.03139, 2016. URL: https://arxiv.org/abs/1609.03139.
  49. Tobias Nipkow. More Church-Rosser Proofs. J. Autom. Reason., 26(1):51-66, 2001. URL: https://doi.org/10.1023/A:1006496715975.
  50. Michael Norrish. Mechanising lambda-calculus using a classical first order theory of terms with permutations. High. Order Symb. Comput., 19(2-3):169-195, 2006. URL: https://doi.org/10.1007/S10990-006-8745-7.
  51. Michael Norrish. Mechanised computability theory. In Marko C. J. D. van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk, editors, Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings, volume 6898 of Lecture Notes in Computer Science, pages 297-311. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22863-6_22.
  52. Frank Pfenning. A Proof of the Church-Rosser Theorem and its Representation in a Logical Framework. Technical Report CMU-CS-92-186, Carnegie Mellon University, 1992. URL: https://apps.dtic.mil/sti/citations/ADA256574.
  53. Gordon D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci., 1(2):125-159, 1975. URL: https://doi.org/10.1016/0304-3975(75)90017-1.
  54. Ole Rasmussen. The Church-Rosser Theorem in Isabelle: A Proof Porting Experiment. Technical Report 164, University of Cambridge, 1995. Google Scholar
  55. Christine Rizkallah, Dmitri Garbuzov, and Steve Zdancewic. A formal equational theory for call-by-push-value. In Jeremy Avigad and Assia Mahboubi, editors, Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, volume 10895 of Lecture Notes in Computer Science, pages 523-541. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94821-8_31.
  56. Natarajan Shankar. A mechanical proof of the Church-Rosser theorem. J. ACM, 35(3):475-522, 1988. URL: https://doi.org/10.1145/44483.44484.
  57. Masako Takahashi. A simple proof of the genericity lemma. In Neil D. Jones, Masami Hagiya, and Masahiko Sato, editors, Logic, Language and Computation: Festschrift in Honor of Satoru Takasu, pages 117-118. Springer Berlin Heidelberg, Berlin, Heidelberg, 1994. URL: https://doi.org/10.1007/BFb0032397.
  58. Masako Takahashi. Parallel reductions in lambda-calculus. Inf. Comput., 118(1):120-127, 1995. URL: https://doi.org/10.1006/INCO.1995.1057.
  59. Chun Tian and Michael Norrish. Mechanising Böhm trees and λη-completeness. In Yannick Forster and Chantal Keller, editors, 16th International Conference on Interactive Theorem Proving (ITP 2025), volume 352 of Leibniz International Proceedings in Informatics (LIPIcs), pages 28:1-28:18, Dagstuhl, Germany, 2025. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2025.28.
  60. Alwen Tiu and Dale Miller. Proof search specifications of bisimulation and modal logics for the pi-calculus. ACM Trans. Comput. Log., 11(2):13:1-13:35, 2010. URL: https://doi.org/10.1145/1656242.1656248.
  61. A. S. Troelstra and Dirk Van Dalen. Constructivism in Mathematics: An Introduction. North Holland, Amsterdam, 1988. Google Scholar
  62. Christian Urban. Nominal techniques in Isabelle/HOL. J. Autom. Reason., 40(4):327-356, 2008. URL: https://doi.org/10.1007/S10817-008-9097-2.
  63. René Vestergaard and James Brotherston. A formalised first-order confluence proof for the lambda-calculus using one-sorted variable names. Inf. Comput., 183(2):212-244, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00023-3.
  64. Christopher P. Wadsworth. Semantics and pragmatics of the lambda-calculus. PhD Thesis, Oxford, 1971. Google Scholar
  65. Christopher P. Wadsworth. The relation between computational and denotational properties for scott’s d_infty-models of the lambda-calculus. SIAM J. Comput., 5(3):488-521, 1976. URL: https://doi.org/10.1137/0205036.
  66. Xinyi Wan and Qinxiang Cao. Formalization of lambda calculus with explicit names as a nominal reasoning framework. In Holger Hermanns, Jun Sun, and Lei Bu, editors, Dependable Software Engineering. Theories, Tools, and Applications - 9th International Symposium, SETTA 2023, Nanjing, China, November 27-29, 2023, Proceedings, volume 14464 of Lecture Notes in Computer Science, pages 262-278. Springer, 2023. URL: https://doi.org/10.1007/978-981-99-8664-4_15.
  67. Hongwei Xi. Upper bounds for standardizations and an application. J. Symb. Log., 64(1):291-303, 1999. URL: https://doi.org/10.2307/2586765.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact