Thunks and Debits in Separation Logic with Time Credits
summary
Machine‑checked reconstruction of Okasaki’s debit reasoning implemented in Iris$, with proofs and reusable artifacts (Zenodo/GitLab). Formalizes the missing deep payment rule and a ghost piggy banks gadget to justify shifting debit from future thunks to earlier ones. Verifies thunk implementation, streams, the physicist’s and implicit queues, and the banker's queue; extract’s spec requires a constant number of time credits, yielding amortized O(1) cost. Proofs handle mutable thunks encoded as references, show sharing of debit views, and come with evaluated artifacts and source proofs.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 0:25Thunks and properties
- 1:51Credits fail for thunks/debits
- 3:15Separation logic with time credits
- 4:16Ghost data structures role
- 6:00Thunk API principles
- 8:47Payment rule significance
- 9:50Streams as nested thunks
- 10:52Banker queue complexity
- 11:33Ghost piggy banks purpose
- 13:18Summary and future work
- 14:00Q&A
related talks
18mDeferring the Details and Deriving Programs
15mDenotational Recurrence Extraction for Amortized Analysis
57mResearch on Different Time Horizons (and an Example with Machine-Checked Proofs)
15mThinking Hard is not Enough
01h 05mAll the Languages Together
01h 06mKeynote – Edwin Brady
19mPanel: Compilation Frameworks
20mPulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs