Towards a Higher-Order Mathematical Operational Semantics
summary
Defines pointed higher-order GSOS laws as dinatural transformations that take syntax as an endofunctor and higher-order behavior as a bifunctor, replacing Turi–Plotkin endofunctor laws. Uses Set (and for lambda calculus Set^F) to model combinatory calculi and call-by-name lambda, proves a general compositionality theorem: the induced operational transition system agrees with a denotational-style model in the sense that strong applicative bisimilarity is a congruence. Notes call-by-value requires sorted sets and the approach yields an executable specification technique.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 0:26Rule Format
- 1:47Plotkin
- 6:59Other Frameworks
- 7:18The Big Problem
- 10:09The primordial problem
- 11:23The framework
- 13:18Proof
- 14:51Framework
- 17:32Application by Similarity
- 18:41Conclusion
- 19:29Questions
related talks
27mBig Steps in Higher-Order Mathematical Operational Semantics
28mTowards Light-Weight Operational Reasoning for Languages with Binders, Categorically
15mStable Relations and Abstract Interpretation of Higher-Order Programs
19mA Pure Demand Operational Semantics with Applications to Program Analysis
12mOn the power of syntactic methods: It is all syntax after all…
27mFunctorial Semantics for Partial Theories
14mAdequacy for Algebraic Effects Revisited
40mFormal semantics for multi-language programs