McTT: Building A Correct-By-Construction Proof Checker For Martin-Loef Type Theory
summary
A correct-by-construction Coq implementation of Martin-Löf type theory produces an end-to-end proof checker, with formalized cumulative universe hierarchy and inductive base naturals, a proven sound and complete normalization-by-evaluation, and a decision procedure for subtyping; the Coq development extracts to readable OCaml of about 20,000 lines that matches skilled human code and runs practical normalization examples far faster than the prior Agda prototype; key claims are mechanized proofs of soundness and completeness of NbE and a verified, efficient type-checker.
AI-written summary · about
chapters (11)
- 0:00McTT introduction and goals
- 3:55Need for verified checker
- 6:47Building McTT challenges
- 9:18Semantic model and normalization
- 11:23Inductive-induction recursion
- 13:59Weakly functional relations
- 15:49Subtyping and universes
- 18:21McTT implementation
- 21:37Normalization performance
- 23:46Conclusion and future
- 26:24Q&A
related talks
01h 03mVerifying Dependent Type-checkers
42mMetaCoq as a tool to prevent future unsoundness in Coq
29mMechanized monadic equational reasoning for ML references
19mExtensible Metatheory Mechanization via Family Polymorphism
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
32mA mechanised and constructive reverse analysis of soundness and completeness of b...
01h 34mFormal Logic Undressed