Extensible Metatheory Mechanization via Family Polymorphism

Explore a 19-minute video presentation from the PLDI 2023 conference that introduces a novel language design for extensible metatheory mechanization in proof assistants. Discover how the researchers leverage family polymorphism, an object-oriented concept, to achieve reusable and extensible code and proofs. Learn about the technical challenges addressed in developing this approach for functional, dependently typed, logical, and interactive proof assistant languages. Examine the prototypical implementation as a Coq plugin, the underlying dependent type theory, and case studies demonstrating its effectiveness in addressing real programming challenges in metatheory mechanization. Gain insights into proof engineering, interactive theorem proving, and solutions to the expression problem in the context of extensible frameworks and inductive types.