Functorial Syntax for All
summary
A Coq library implements a variant of Fiore–Plotkin–Turi functorial syntax: users define syntax as functors over indexing categories and supply functorial and monadic actions that model mapping and parallel substitution. The library provides a hierarchy of type classes, tactics for routine proofs, and instantiations for sets, typed contexts, products, and linear settings. It works for many formalisations (including lambda-mu and a System T example), enables NBE-style constructions and CPS reasoning, but a fully intrinsic System F encoding becomes unwieldy.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:28Historical foundations
- 4:43Well-scoped syntax in Coq
- 7:10Intrinsically typed syntax in Coq
- 9:17Modular syntax library
- 11:44Extensibility via indexing
- 13:12Advanced linear syntax
- 15:23Limitations and challenges
- 16:52Normalization by evaluation
- 17:58Boilerplate automation
- 19:34Q&A
related talks
23mImplementing a category-theoretic framework for typed abstract syntax
27mFunctorial Semantics for Partial Theories
23mFormalizing Monoidal Categories and Actions for Syntax with Binders
26m2-Functoriality of Initial Semantics, and Applications
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
19mExtensible Metatheory Mechanization via Family Polymorphism
46mProfunctor Optics: The Categorical Approach
02h 24mCategory Theory Track