Coq a la Carte: A Practical Approach to Modular Syntax With Binders
summary
Presents a Coq workflow that achieves practical modular syntax by using direct injections of variant copies instead of functor fixed points, plus generated boilerplate and a small tactic suite (MetaCoq-like) to assemble features. Implements inductive types, recursive functions and predicates, and proves preservation and strong normalization for a lambda calculus extended with booleans and arithmetic. Case study totals ≈1,000 lines for features + ≈200 lines for the variant, works but needs custom induction principles and a few global lemmas.
AI-written summary · about
chapters (5)
- 0:00Start
- 5:36Contribution A Practical Aproach to Modular Syntax
- 9:00Modular Recursive Functions
- 11:02General Framework and Tool Support
- 12:00Start with a specification
related talks
19mExtensible Metatheory Mechanization via Family Polymorphism
01h 34mFormal Logic Undressed
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
42mMetaCoq as a tool to prevent future unsoundness in Coq
19mInterpreting OCaml GADTs into Coq
21mFunctorial Syntax for All
31mA Coq Library of Undecidable Problems