All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants
summary
Adds a principled sort quantifier that generalizes Prop, Type, and SProp and is implemented in Coq with a new sort-polymorphic prelude that replaces duplicated definitions like prod and lists. Proves a monomorphization theorem so every sort-polymorphic term can be expanded into ground instantiations, gives a parametricity translation for sort quantification, and successfully ports the setoid rewrite tactic to handle Prop/Type/SProp. Reports improved elaboration and reusable artifacts.
AI-written summary · about
chapters (25)
- 0:00Introduction
- 0:22Problem solved
- 1:05Proof assistants
- 2:13Sorts in Rocq
- 3:19Duplication in Rocq
- 4:23Lean’s partial solution
- 5:50Pinx quantification
- 6:33Sort polymorphic identity
- 7:17Sort polymorphic products
- 7:38Sort polymorphic booleans
- 8:44Large elimination
- 9:48Adoption challenges in Rocq
- 10:09Sort polymorphic prelude
- 10:51Sort polymorphic lists
- 11:12Case study: setoid rewrite
- 12:15Theoretical properties
- 13:00Monomorphization
- 13:42Parametricity
- 14:04Future integration
- 14:47Extending proof assistants
- 15:30Performance improvements
- 16:38Instantiating sort theories
- 17:42Elimination constraints
- 18:25Monomorphization theorem
- 19:07Migration to prelude
related talks
19mExtensible Metatheory Mechanization via Family Polymorphism
15mTowards a Coq Specification for Generalized Algebraic Datatypes in OCaml
35mHow to make ad hoc proof automation less ad hoc
21mPolymorphic Type Inference for Dynamic Languages
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
24mAn Order-Theoretic Analysis of Universe Polymorphism
19mAutomated Verification of Fundamental Algebraic Laws
46mAdding kind-polymorphism to the Scala programming language