References

• The Lean Language Reference
• Lean Game Server
• mathlib4
• PhysLean
• Benjamin Pierce
  • Software Foundations, Resources
• Jeremy Avigad, Books
• Wen-Tsun Wu, Mechanical Theorem Proving in Geometries
• Franka Waaldijk
• Kevin Buzzard, Formalizing Mathematics
• Terence Tao, A Lean companion to Analysis I
• L. E. J. Brouwer
• Errett Bishop
• Per Martin-Löf
• Jean-Yves Girard
  • Girard's paradox: Type : Type is inconsistent.
  • Linear Logic
  • Geometry of Interaction
  • Transcendental Syntax
• Thierry Coquand
• Xavier Leroy
• John C. Baez
• William Lawvere
• Type theorists: Andrej Bauer, Egbert Rijke, Jonathan Sterling, Carlo Angiuli, Daniel Gratzer, Kuen-Bang Hou (Favonia), Robert Harper, Simon Huber, Anders Mörtberg, Thorsten Altenkirch, Ambrus Kaposi, Daniel Licata, Mike Shulman, Peter LeFanu Lumsdaine, Frank Pfenning
• Leibniz's characteristica universalis
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Cubical Type Theory
• Higher Observational Type Theory
• Dependent Linear Type Theory
• Conor McBride, I Got Plenty o’ Nuttin’
• Robert Atkey, Syntax and Semantics of Quantitative Type Theory
• Idris 2
  • Oleg Grenrus, Dependent Linear types in QTT
• David Jaz Myers, Structure-aware version control via observational bridge types
• Cubical Agda
• The ATS Programming Language
  • "A (Not So Gentle) Introduction To Systems Programming In ATS" by Aditya Siram
  • Bluish Coder
  • Encoding web application specifications using Haskell and ATS
  • learnats.dats
• CompCert
• sel4
  • Tuna Cici, seL4 Microkernel: Architecture
• SPARKNaCl
• HACL*