McTT: A Verified Kernel for a Proof Assistant
summary
A fully verified kernel for core Martin‑Löf type theory is implemented in Rocq, proving normalization, consistency and injectivity of constructors and proving soundness and completeness of a normalization‑by‑evaluation based type checker with a full cumulative universe hierarchy. The project extracts an extracted OCaml kernel coupled to an unverified lexer and pretty‑printer, amounts to 20,000 lines (10,000 excluding proofs), and successfully type‑checks a suite of small examples while handling induction‑recursion encoding without Bob‑Capa.
AI-written summary · about
chapters (9)
- 0:00McTT introduction and motivation
- 2:35Verifying the kernel itself
- 4:01McTT structure and components
- 6:57Implementation challenges
- 9:29Induction-recursion in Rocq
- 13:08Algorithmic type checking
- 16:39Verified human-readable implementation
- 18:26McTT contributions and future
- 20:33Q&A on trust and comparisons