Higher-Order Behavioural Conformances via Fibrations
summary
Categorical framework defines an abstract higher-order specification (AHOS) for big-step semantics and models program conformance via fibrations; behavioural notions lift to the fibre using concrete constructions like the Kantorovich lifting for distributions. Main theorem: under natural “niceness” conditions the greatest behavioural conformance (bisimilarity, pseudometrics) on the operational model is a congruence. Covers probabilistic lambda calculus, rederives contextual pseudometric bounds (e.g. omega vs ½-terminating yields distance 0.5) and uses Kantorovich–Wasserstein duality in the niceness checks.
AI-written summary · about
chapters (16)
- 0:00Program behavioral equivalence
- 1:47Quantitative distances in probabilistic languages
- 3:12Computing contextual pseudometrics
- 4:55History of applicative bisimulations
- 7:02Applicative pseudometrics and Howe method
- 9:53Limitations of coinductive techniques
- 10:13Categorical syntax and semantics
- 13:04Higher-order operational specifications
- 15:12Generalizing applicative conformances via fibrations
- 17:40Fibrations for conformances
- 19:47Congruence for applicative conformances
- 21:34Applications to probabilistic languages
- 22:18Higher-order operational semantics
- 23:01Q&A: Relation to prior work
- 24:23Q&A: Howe method
- 25:30Q&A: Applicative vs normal form
related talks
27mBig Steps in Higher-Order Mathematical Operational Semantics
24mTowards a Higher-Order Mathematical Operational Semantics
49mSemantic Foundations for Probabilistic Programming
14mAdequacy for Algebraic Effects Revisited
15mStable Relations and Abstract Interpretation of Higher-Order Programs
21mRelating Distances and Abstractions: An Abstract Interpretation Perspective
18mEquivalence and Similarity Refutation for Probabilistic Programs
28mTowards Light-Weight Operational Reasoning for Languages with Binders, Categorically