Barendregt's genericity lemma (1984) is a classic result in the theory of the λ-calculus, formalizing the fact that meaningless terms are sort of black holes for evaluation: if evaluation should ever enter them, it would never get out. Ten years later, in 1994, Takahashi publishes a two-page paper titled "A Simple Proof of the Genericity Lemma". Many other proof developments now exist, including an 8-line proof using Taylor Expansion (Barbarossa-Manzonetto 2020) and genericity lemmas for call-by-value evaluation (Accattoli-Lancelot 2024; Arrial-Guerrieri-Kesner 2024; ...).

In this talk, I will explain why genericity is a cornerstone result in Barendregt's book and why I think it is still relevant today (in particular viewed as a result on program preorders). I will overview the different possible proof techniques and tell you about our formalization in the Abella proof assistant of Takahashi's technique: a two-page paper turns into roughly 2500 lines of code.

The end of the talk will hopefully mention open questions and future work on the topic.

Based on: Light Genericity, FoSSaCS 2024 https://link.springer.com/chapter/10.1007/978-3-031-57231-9_2; Barendregt's Theory of the λ-calculus, Refreshed and Formalized, ITP 2025 https://doi.org/10.4230/LIPIcs.ITP.2025.13; and my PhD thesis, 2025 https://theses.hal.science/tel-05407883