Verifying Dependent Type-checkers
summary
Formal verification of a dependent type-checker for a Coq-like calculus (Metarok) uses assumed normalization axioms and yields concrete wins: it found a bug in the Coq kernel tied to dependent pattern-matching, universes and cumulativity (8.7–8.13), and drove a binder redesign and a completeness proof. The work formalizes typed versus term-directed conversion, proves positive and negative soundness separately, explains unit/unit‑like pitfalls, produces a verified extraction pipeline (lambda_box) and costs multiple person‑years. Metarok verified checker assumes normalization axioms.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 8:24Type system verification
- 10:11Metarok and pattern matching
- 23:55Metarok bug hunt
- 24:16Conversion checking algorithms
- 46:35Verification benefits and challenges
- 51:28Progress and future directions
- 53:24Q&A
related talks
36mMcTT: Building A Correct-By-Construction Proof Checker For Martin-Loef Type Theory
42mMetaCoq as a tool to prevent future unsoundness in Coq
01h 26mImplementing Dependent Pattern Matching and Type Unification Part 2
29mType Checking with Rewriting Rules
46mThe Calculated Typer (Functional Pearl)
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
19mExtensible Metatheory Mechanization via Family Polymorphism
22mSafe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting