Towards Verification of a Denotational Semantics of Inheritance
summary
An Agda formalisation replicates the OOPSLA ’89 operational and denotational definitions of inheritance, uses Agda proof assistant to check the equivalence via a step-indexing fuel pattern, and successfully type-checks all lemma proofs under the same assumptions about recursively defined Scott domains and continuity. The mechanisation exposes three issues detected in the original paper (a maybe/parent misuse, calling numbers as objects, and a trivial double‑use bug), and the verified Agda development completes and validates the original fixed‑point reasoning.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:57Yen's early career
- 4:57Denotational semantics and fixpoints
- 10:17Inheritance semantics
- 13:13Bugs in semantics
- 16:07Agda demo
- 18:58Fuel-based verification
- 20:46Conclusion
- 21:50Q&A
related talks
34mChecking a Denotational Semantics of Scheme in Agda
19mAutomated Verification of Fundamental Algebraic Laws
14mAdequacy for Algebraic Effects Revisited
15mStable Relations and Abstract Interpretation of Higher-Order Programs
19mDeriving Dependently-Typed OOP from First Principles
16mA Hoare-Logic Style Refinement Types Formalisation
19mExtensible Metatheory Mechanization via Family Polymorphism
30mFormal Metatheory of Second-Order Abstract Syntax