Contextual Algebraic Theories: Generic Boilerplate beyond Abstraction
summary
Menkar faces massive duplicated boilerplate across renaming, substitution, normalization and pretty‑printing; the proposal defines Contextual Multisorted Algebraic Theories as a direct generalization of SOMATs to let context extensions be arbitrary junctures (supporting multimodal simple type theory, dual‑context systems, context exponentiation and a right adjoint). Equation‑free CMATs are partly formalized, the equationful/substitution theorems are being adapted from Fiore/Szawomzavencev, and the work is formalized in Cubical Agda with the goal of generic safe NbE and practical reuse in Menkar.
AI-written summary · about
chapters (9)
- 0:00Contextual algebraic theories
- 2:05Existing approaches
- 3:51Equation-free algebraic theories
- 5:14Multi-sorted algebraic theories
- 6:18Second-order algebraic theories
- 8:24Limitations of systems
- 9:47Junctures and contextual theories
- 10:29Formalizing contextual theories
- 11:52Q&A
related talks
12mA Unified View of Modalities in Type Systems
22mMoebius: Metaprogramming using Contextual Types
19mExtensible Metatheory Mechanization via Family Polymorphism
30mFormal Metatheory of Second-Order Abstract Syntax
11mLocal algebraic effect theories
14mType-Sensitive Algebraic Macros
26mThe Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic(…)
29mMechanized monadic equational reasoning for ML references