All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants

Explore a 20-minute conference talk from POPL 2025 that addresses a fundamental challenge in proof assistant design: how to handle polymorphism across different universe sorts in dependent type theory. Learn how researchers from Inria and the University of Chile developed a comprehensive theory of sort polymorphism to enhance reusability and extensibility in proof assistants like Coq, Lean, and Agda. The presentation covers the theoretical foundations and practical implementation of sort polymorphism, including monomorphization, large elimination, and parametricity. Discover how this approach creates a more flexible framework for multi-sorted type theories, demonstrated through a new sort-polymorphic prelude of basic definitions and automation in Coq. The talk includes supplementary materials that have been evaluated as reusable artifacts, making it valuable for researchers and developers working with proof assistants and type theory.