Enhancing universe polymorphism for Rocq: Algebraic universes, consistency checking(…)
summary
Mechanical refinement of Bezem–Coquand’s decision procedure is implemented and machine-verified inside a Rocq branch, producing a concrete universe model and an API that accepts algebraic universes (0, +1, max) and performs polynomial-time satisfiability and validity checks with incremental loop detection. The implementation removes the old refresh-universes dance, enables direct substitution/instantiation during elaboration, and exposes a variance-based minimization that drops irrelevant universe constraints. Preliminary experience reuses a state-of-the-art solver that previously yielded ~30% faster checks and shows substantially fewer fresh levels and constraints in polymorphic cumulativity.
AI-written summary · about
chapters (8)
- 0:00Universe polymorphism in Rocq
- 1:58Universe unification challenges
- 3:22Efficient type inference constraints
- 6:10Consistency checking algorithm
- 9:21New model implementation
- 12:12Universe variance and minimization
- 14:01Working with polymorphism modes
- 14:22Q&A on unification
related talks
19mCertified Compilers à la Carte
24mAn Order-Theoretic Analysis of Universe Polymorphism
22mComputing Solutions for Systems of Multivariate Ordinary Differential Equations in Rocq
46mMechanizing Abstract Interpretation
01h 03mVerifying Dependent Type-checkers
23mTowards Verifiable System Code using a DSL Compiled to Efficient and Readable C Code
51mElpi: rule-based meta-languge for Rocq
20mFormalizing polynomial laws and the universal divided power algebra