Formal Metatheory of Second-Order Abstract Syntax
summary
An Agda-based generator turns a concise syntax signature into an Agda code generator that produces an intrinsically-encoded inductive datatype plus weakening, single-variable substitution, and metasubstitution and second-order rewriting operations with their proofs derived automatically. Initial-algebra semantics yields compositional semantic maps and the substitution lemma by construction. The system emits a few lines of boilerplate per constructor, handles second-order axioms (examples include first-order logic with metavariables), and currently excludes linear or dual-context extensions.
AI-written summary · about
chapters (12)
- 0:00Start
- 2:36Syntax Description File
- 3:39Overview
- 4:49Intrinsic Encoding
- 5:23Context Map
- 10:51Single Variable Substitution
- 11:59Recap
- 12:45Pointed Sigma Algebras
- 13:13Homomorphism Conditions
- 19:43The Syntax of First Order Logic
- 24:10Why Did You Use a Script To Generate the Syntax Data Types Instead of Using a Single Definition of Abstract Binding Trees
- 25:08Are There Limitations to the Kind of Syntax Your Library Can Handle
related talks
28mSynthesizing Abstract Transformers
12mContextual Algebraic Theories: Generic Boilerplate beyond Abstraction
16mA Hoare-Logic Style Refinement Types Formalisation
23mImplementing a category-theoretic framework for typed abstract syntax
14mType-Sensitive Algebraic Macros
16mAutomatically Deriving Control-Flow Graph Generators from Operational Semantics
23mFormalizing Monoidal Categories and Actions for Syntax with Binders
12mOn the power of syntactic methods: It is all syntax after all…