4. Bibliography🔗

The works below are cited throughout the notes. Academic references use Verso's citation system; books, lecture notes, and online resources are modelled as @misc-style entries. Each title links to the source.

• Jeremy Avigad, Leonardo de Moura, Soonho Kong, and Sebastian Ullrich, 2024. “Theorem Proving in Lean 4”. In Online textbook.

• Kevin Buzzard and Bhavik Mehta, 2024. “Formalising Mathematics”. In Online lecture notes.

• Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg, 2018. “Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom”. arXiv:1611.02108

• Thierry Coquand and Gérard Huet (1988). “The Calculus of Constructions”. Information and Computation.76 2–3pp. 95–120.

• Thierry Coquand and Christine Paulin-Mohring, 1990. “Inductively Defined Types”. In COLOG-88. (Lecture Notes in Computer Science 417)

• Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer, 2015. “The Lean Theorem Prover (System Description)”. In Automated Deduction – CADE-25. (Lecture Notes in Computer Science 9195)

• Leonardo de Moura and Sebastian Ullrich, 2021. “The Lean 4 Theorem Prover and Programming Language”. In Automated Deduction – CADE 28. (Lecture Notes in Computer Science 12699)

• Jean-Yves Girard, 1972. Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur. PhD thesis, Université Paris VII

• Per Martin-Löf, 1975. “An Intuitionistic Theory of Types: Predicative Part”. In Logic Colloquium '73. (Studies in Logic and the Foundations of Mathematics 80)

• The mathlib Community, 2020. “The Lean Mathematical Library”. In CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs.

• The mathlib Community, 2025. “Mathlib Documentation”. In Online API documentation.

• The Univalent Foundations Program, 2013. “Homotopy Type Theory: Univalent Foundations of Mathematics”. In Institute for Advanced Study.