-
Notifications
You must be signed in to change notification settings - Fork 0
References
KUO-TSAN HSU (Gordon) edited this page Nov 12, 2025
·
5 revisions
- 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 : Typeis inconsistent. - Linear Logic
- Geometry of Interaction
- Transcendental Syntax
- Girard's paradox:
- 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
- CompCert
-
sel4
- Tuna Cici, seL4 Microkernel: Architecture
- SPARKNaCl
- HACL*