Bounded Sort Polymorphism with Elimination Constraints

on YouTube ↗23m

" summary

Extends sort polymorphism with elimination constraints that record which sorts may eliminate into which, implements the system in the Rocq prover, and proves relative consistency by instantiating sort variables to dominated ground sorts (with an added initial data sort when necessary). Delivers algorithmic principal sort assignment and an elaborator that reconstructs those bounds; artifacts and an RFC exist; the Rocq prototype works but shows some performance regressions due to graph-based eliminability checks.

AI-written summary · about

" chapters (12)

1. 0:00Bounded sort polymorphism intro
2. 1:51Multi-sorted type theories issues
3. 5:43Sort polymorphism without bounds
4. 8:13Manual eliminator declaration problems
5. 9:16Bounds in sort polymorphism
6. 9:57Consistency with sort poly system
7. 13:14Conversion rules and theorem
8. 14:42Consistency theorem conditions
9. 18:33Instantiating sort variables
10. 19:36Rocq implementation
11. 20:59Future work and extensions
12. 21:20Q&A