A Simple and Efficient Implementation of Strong Call by Need by an Abstract Ma…
summary
Claims a concrete abstract machine called RKNL that implements strong call-by-need by automatically transforming a higher-order evaluator (with memothunks) using an off‑the‑shelf functional‑correspondence tool, producing an 11‑rule, environment+stack+store machine with two levels of memoization. It proves quasilinear cost in initial term size and number of normal‑order beta steps (improving quadratic→quasilinear), uses a potential‑function proof, measures steps empirically, and avoids size‑explosion via implicit sharing.
AI-written summary · about
chapters (13)
- 0:00Intro
- 0:15Why call by need?
- 1:10Why strong reduction?
- 2:47In what sense efficient?
- 5:16Further Plan of the Presentation
- 6:17Functional Correspondence
- 8:43Derivation
- 11:06Correctness and Complexity
- 12:28Ghost Abstract Machine
- 14:02Potential Function
- 15:53Empirical Method
- 16:23Size Explosion Problem
- 17:12Summary
related talks
21mAn OCaml use case for strong call-by-need reduction
36mFlexible Instruction-Set Semantics via Abstract Monads
15mStable Relations and Abstract Interpretation of Higher-Order Programs
18mDeveloping a Dependently Typed Language with Runtime Proof Search
11mThe full-reducing Krivine abstract machine KN simulates pure normal-order reduction i...
41mConcatenative programming and stack-based languages
19mA Pure Demand Operational Semantics with Applications to Program Analysis
29mMechanized monadic equational reasoning for ML references