Normalisation for First-Class Universe Levels
summary
Proves normalization for a dependent type theory with first-class universe levels and derives decidable equality, decidable type-checking and canonicity; shows level primitives can be erased when extracting to an untyped lambda calculus while preserving reduction. Uses an inductive-recursive logical relation over an extrinsically typed syntax, formalises the development and proofs formalized in Agda, builds on the graded type theory project, and produces machine-checked artifacts that yield decidable type-checking and weak-head/full normalization.
AI-written summary · about
chapters (16)
- 0:00First-class universe levels
- 2:22Universe stratification necessity
- 4:32Avoiding universe duplication
- 5:58Agda's universe levels
- 7:27Meta-theory of first-class levels
- 9:58Normalization in proof assistants
- 11:05Normalization in Agda
- 12:31Inductive-recursive approach
- 14:19Universe levels syntax
- 15:45Universes type structure
- 17:35Reducibility judgments
- 21:39Conclusion and future work
- 23:29Q&A: Recursive reductions
- 25:58Q&A: Bounded quantification
- 27:31Q&A: Models for levels
- 28:13Q&A: Comparison with Tarski universes
related talks
23mNormalizable types
26mObservational Equality: Now for Good
24mAn Order-Theoretic Analysis of Universe Polymorphism
20mA Dependent Type Theory for Meta-programming with Intensional Analysis
23mImpredicative Observational Equality
01h 03mVerifying Dependent Type-checkers
24mA Formalization of Opaque Definitions for a Dependent Type Theory
15mStable Relations and Abstract Interpretation of Higher-Order Programs