Towards Light-Weight Operational Reasoning for Languages with Binders, Categorically
summary
Proposes representing substitution as a runtime operator by translating lambda calculus into a new combinatory lambda calculus with an operator for each lambda term, builds small‑step operational semantics for that infinite signature, and proves the translations back and forth preserve behavior up to strong applicative similarity. Uses higher‑order categorical GSOS machinery, contrasts running the framework in presheaves versus working directly in Sets after translation, and delivers a formal theorem equating the original and combinatory dynamics while noting this is work in progress.
AI-written summary · about
chapters (10)
- 0:00Lightweight operational reasoning
- 1:04Contextual equivalence methods
- 3:14Categorical abstraction
- 7:13Higher-order semantics
- 11:34Combinatory logic example
- 15:49Binders challenges
- 19:00Combinatorial lambda proposal
- 23:20Generalizing correspondence
- 25:50Future directions
- 26:11Q&A
related talks
24mTowards a Higher-Order Mathematical Operational Semantics
23mFormalizing Monoidal Categories and Actions for Syntax with Binders
15mStable Relations and Abstract Interpretation of Higher-Order Programs
37mClassical Processes in modern dress
27mBig Steps in Higher-Order Mathematical Operational Semantics
59mUnification Modulo Equational Theories in Languages with Binding Operators
12mOn the power of syntactic methods: It is all syntax after all…
23mImplementing a category-theoretic framework for typed abstract syntax