Barendregt's Theory of the λ-Calculus, Refreshed and Formalized. - Adrienne Lancelot; Beniamino Accattoli; Maxime Vemclefs (ITP, 2025)