Every external source cited anywhere in this book, consolidated into one list with one consistent citation style. Each chapter’s own “References” section links back to the entries it uses, with a short note on why that source is cited at that specific spot — this page holds the full citation, once, for every source in the book. (This does not include the Lean tactic-reference/Loogle links used inline throughout the main text, or Mathlib module paths named in “Mathlib equivalent” boxes — those serve as functional, per-occurrence documentation links rather than citations, and are indexed separately in the tactic and library reference.)
[Aluffi2009] Paolo Aluffi, Algebra: Chapter 0, Graduate Studies in Mathematics vol. 104, American Mathematical Society, 2009.
[AssemSimsonSkowronski2006] Ibrahim Assem, Daniel Simson, and Andrzej Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1: Techniques of Representation Theory, London Mathematical Society Student Texts 65, Cambridge University Press, 2006.
[Chlipala2013] Adam Chlipala, Certified Programming with Dependent Types, MIT Press, 2013. Free online edition.
[Church1941] Alonzo Church, The Calculi of Lambda-Conversion, Princeton University Press, 1941.
[CoquandHuet1988] Thierry Coquand and Gérard Huet, “The Calculus of Constructions,” Information and Computation, 76(2–3), 1988, 95–120.
[DummitFoote2003] David S. Dummit and Richard M. Foote, Abstract Algebra, 3rd ed., Wiley, 2003.
[Gentzen1935] Gerhard Gentzen, “Untersuchungen über das logische Schließen,” Mathematische Zeitschrift, 1935.
[Godel1930] Kurt Gödel, “Die Vollständigkeit der Axiome des logischen Funktionenkalküls,” 1930.
[Girard1971] Jean-Yves Girard, “Une extension de l’interprétation de Gödel à l’analyse, et son application à l’élimination des coupures dans l’analyse et la théorie des types,” in Proceedings of the Second Scandinavian Logic Symposium, Studies in Logic and the Foundations of Mathematics vol. 63, North-Holland, 1971, 63–92.
[Howard1980] William A. Howard, “The Formulae-as-Types Notion of Construction,” in To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, 1980, 479–490. (Circulated privately since 1969.)
[HoTT2013] The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics, 2013. Free online.
[Jacobs1999] Bart Jacobs, Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics vol. 141, Elsevier, 1999.
[LeanDocs] Lean 4 documentation, “Basic Types” and the Tactic Reference.
[Mathlib4Docs] Mathlib4 API documentation.
[MacLane1998] Saunders Mac Lane, Categories for the Working Mathematician, 2nd ed., Graduate Texts in Mathematics 5, Springer, 1998.
[MartinLof1984] Per Martin-Löf, Intuitionistic Type Theory, Bibliopolis, 1984.
[Milner1978] Robin Milner, “A Theory of Type Polymorphism in Programming,” Journal of Computer and System Sciences, 17(3), 1978, 348–375.
[MypyDocs] mypy documentation.
[Pareigis1970] Bodo Pareigis, Categories and Functors, Pure and Applied Mathematics vol. 39, Academic Press, 1970.
[Pierce2002] Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002.
[PierceSF] Benjamin C. Pierce et al., Software Foundations, Volume 1: Logical Foundations, softwarefoundations.cis.upenn.edu.
[PythonTyping] Python typing module documentation, TypeVar.
[Rojas2015] Raúl Rojas, “A Tutorial Introduction to the Lambda Calculus,” 2015.
[Schiffler2014] Ralf Schiffler, Quiver Representations, CMS Books in Mathematics, Springer, 2014.
[Thompson1991] Simon Thompson, Type Theory and Functional Programming, Addison-Wesley, 1991. Freely available from the author’s institutional repository. (⚠ Link check 2026-07-19: kar.kent.ac.uk failed to complete a TLS handshake while the parent kent.ac.uk domain and unrelated control sites responded normally — possibly a dead/misconfigured host for the Kent Academic Repository subdomain specifically. Worth a manual check before relying on this link.)
[TPIL4] Theorem Proving in Lean 4, “Dependent Type Theory” (§2.1 “Simple Type Theory,” §2.8 “What makes dependent type theory dependent?”) and “Propositions and Proofs” (§3.1 “Propositions as Types”). (URLs verified 2026-07-19; the book’s original links used a stale pre-rewrite URL scheme — dependent_type_theory.html etc. — which now 404s.)
[VanDalen2013] Dirk van Dalen, Logic and Structure, 5th ed., Springer, 2013.
[Weibel1994] Charles A. Weibel, An Introduction to Homological Algebra, Cambridge Studies in Advanced Mathematics 38, Cambridge University Press, 1994.