Tealeaves: Categorical structures for syntax
summary
Tealeaves is a Coq library that provides a typeclass for syntax-like datatypes based on decorated-traversable monads and exposes a context-sensitive iterator bind_dt with an equational theory. A locally nameless backend is implemented and used to formalize STLC and System F, with progress and preservation proofs checked; a multi-sorted generalization is sketched. Backends must supply the bind_dt instance for a concrete var/binder representation; automated instance synthesis remains future work.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 0:33Outline
- 0:54Formal systems
- 1:19Syntax infrastructure
- 2:22Types of representations
- 3:46Thought experiment
- 5:28Tealeaves
- 6:24Syntax
- 7:44Decorativetraversable monads
- 12:21Binding DT
- 15:05Using Tealeaves
- 15:52Brownbackend
- 16:58Automated workflow
- 18:03Localized backend
- 18:59Virtual questions
related talks
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
14mType-Sensitive Algebraic Macros
30mComputation-Tree Semantics: An Algorithmic Approach to Structurally Defined Relations
21mFunctorial Syntax for All
17mTEAL: a Total Expressive Assembly Language
24mChoice Trees: Representing Nondeterministic, Recursive, and Impure Programs in C...
21mTail Modulo Cons, OCaml, and Relational Separation Logic
20mA Dependent Type Theory for Meta-programming with Intensional Analysis