← All papers
The Type Theory of Lean
cs.LO
Jan 1, 2020 · v1
TL;DR
Provides a formal specification of Lean's kernel type theory and metatheoretic properties.
Abstract
This master's thesis describes the type theory underlying the Lean theorem prover, providing a formal specification of the calculus of inductive constructions as implemented in Lean. It covers the kernel type system, soundness, and normalization properties of the system.
Problem
The Lean theorem prover needs a rigorous formal specification of its underlying type theory to establish trust in its kernel and enable independent verification of its soundness.
Approach
This master's thesis describes the type theory underlying the Lean theorem prover, providing a formal specification of the calculus of inductive constructions as implemented in Lean. It covers the kernel type system, soundness, and normalization properties.
Results
The thesis provides a complete formal specification of Lean's type theory, covering inductive types, universes, and reduction rules, serving as a reference for the system's metatheoretic properties.