Extensible Metatheory Mechanization via Family Polymorphism
summary
Claims a language-layer for family polymorphism inside Coq that reuses code and proofs via late binding and generates a Coq plugin plus a core dependent type theory with proved consistency and canonicity. Implements F_inductive, F_recursion/F_induction, automatic propositional equalities for case handlers, a partial eliminator and F_discriminate/F_injection tactics; enforces declaration order to forbid cycles. Case studies port Software Foundations proofs, add four STLC extensions and compose them, and build abstract-interpreter families — implementation reuses compiled modules without recompilation.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:16Extensible metatheory mechanization
- 3:02Family polymorphism in FPop
- 5:13Dependently typed proof challenges
- 7:43Equational reasoning with late binding
- 9:56Partial eliminators for extensible types
- 11:03Logical consistency in FPop
- 11:46Coq plugin implementation
- 13:35Proof engineering case studies
- 15:24Family polymorphism in MLTT
- 16:14Limitations and future work
- 16:57Conclusion and Q&A
related talks
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
22mMoebius: Metaprogramming using Contextual Types
20mAll Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
24mAn Intrinsically-typed Probabilistic Programming Language in Coq (Extended Abstr...
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
21mPolymorphic Type Inference for Dynamic Languages