Ctrl+K

References & further reading

References & further reading#

A curated, tiered reading list for the whole course. The bibliography below is generated from references.bib.

Core#

  • Sørensen & Urzyczyn, Lectures on the Curry–Howard Isomorphism — the spine of Lectures 1–3.

  • Barendregt, The Lambda Calculus — the reference for Lecture 2.

  • Riehl, A Reintroduction to Proofs (Lean game) — the backbone of Lecture 3.

  • Macbeth, The Mechanics of Proof & the Natural Number Game — Lecture 4.

  • Mathlib documentation and the Lean community pages — Lectures 4–6.

Supplementary#

  • Girard, Lafont & Taylor, Proofs and Types.

  • Pierce, Types and Programming Languages.

  • Nederpelt & Geuvers, Type Theory and Formal Proof.

  • Avigad, Mathematical Logic and Computation.

Advanced / foundations#

  • Martin-Löf, Intuitionistic Type Theory.

  • The Univalent Foundations Program, Homotopy Type Theory.

  • Church (1936, 1940) and Howard (1980) — the primary sources.

Capstone#

  • Odrzywołek, All elementary functions from a single binary operator (arXiv:2603.21852), with its Lean 4 formalization.

Full bibliography#

[Avi22]

Jeremy Avigad. Mathematical Logic and Computation. Cambridge University Press, 2022.

[Bar84]

Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, revised edition, 1984.

[BP+]

Kevin Buzzard, Mohammad Pedramfar, and others. The natural number game. URL: https://adam.math.hhu.de/#/g/leanprover-community/nng4.

[Chu36]

Alonzo Church. An unsolvable problem of elementary number theory. American Journal of Mathematics, 58(2):345–363, 1936.

[Chu40]

Alonzo Church. A formulation of the simple theory of types. The Journal of Symbolic Logic, 5(2):56–68, 1940.

[GLT89]

Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types. Cambridge University Press, 1989.

[How80]

William A. Howard. The formulae-as-types notion of construction. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479–490. Academic Press, 1980.

[Mac23]

Heather Macbeth. The mechanics of proof. 2023. URL: https://hrmacbeth.github.io/math2001/.

[MLof84]

Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984.

[NG14]

Rob Nederpelt and Herman Geuvers. Type Theory and Formal Proof: An Introduction. Cambridge University Press, 2014.

[Odrzywolek26]

Andrzej Odrzywołek. All elementary functions from a single binary operator. 2026. arXiv:2603.21852; Lean 4 formalization: github.com/nasqret/eml-formalization. URL: https://arxiv.org/abs/2603.21852.

[Pie02]

Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002.

[Rie24]

Emily Riehl. A reintroduction to proofs (lean game). 2024. URL: https://adam.math.hhu.de/#/g/emilyriehl/ReintroductionToProofs.

[SorensenU06]

Morten Heine Sørensen and Paweł Urzyczyn. Lectures on the Curry–Howard Isomorphism. Elsevier, 2006.

[TheMCommunity]

The Mathlib Community. Mathlib: the lean mathematical library. URL: https://leanprover-community.github.io/.

[TheUFProgram13]

The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. URL: https://homotopytypetheory.org/book/.

Contents