Checking a Denotational Semantics of Scheme in Agda
summary
A shallow embedding of the R5RS denotational semantics into Agda is implemented and type-checked, revealing concrete well-formedness bugs (including a missing Kappa parameter in call-with-values and dubious overloading of true/false), plus cycles that force breaking expressed-value definitions. The Agda model relies on several unsound postulates to get bottoms and fixed points but successfully flags problems and drives suggested edits to the standard; artifact and code are available. shallow embedding R5RS denotational semantics
AI-written summary · about
chapters (7)
- 0:00Denotational semantics intro
- 3:36Shallow embedding in Agda
- 9:33Abstract syntax in Agda
- 15:51Semantic equations
- 19:21Well-formedness issues
- 22:32Conclusion
- 23:59Q&A
related talks
24mTowards Verification of a Denotational Semantics of Inheritance
15mStable Relations and Abstract Interpretation of Higher-Order Programs
19mSo You Want To Analyze Scheme Programs With Datalog?
18mCertified Semantics for Disequality
25mShallowly embedding type theories
30mFormal Metatheory of Second-Order Abstract Syntax
01h 03mVerifying Dependent Type-checkers
14mAdequacy for Algebraic Effects Revisited