Higher-Order Weakest Precondition Transformers via a CPS Transformation
summary
Claims that generic weakest preconditions for a higher‑order language with effects and recursion are computable syntactically by a CPS transformation, using algebraic effects and monadic semantics to map effectful programs to formulas in a higher‑order logic with modal operators and fixed points. Builds an explicit CPS mapping that turns continuations into truth‑valued postconditions, proves equality with the semantic weakest‑precondition construction, and successfully recovers instances like expected cost analyses, trace/may‑must reachability and a new cost‑moment analysis.
AI-written summary · about
chapters (10)
- 0:00Weakest precondition transformers
- 1:07Weakest precondition conditions
- 6:10Instances of weakest preconditions
- 9:06Semantic framework for weakest preconditions
- 12:21Syntactic weakest precondition computation
- 14:13General CPS transformation theorem
- 18:17CPS transformation explained
- 21:08Theorem instances
- 24:33Comparison with Dexter Monad
- 25:57Q&A
related talks
12mTowards Dependently-Typed Control Effects (Extended Abstract)
19mTowards a Reflection for Effect Handlers
13mOne-Pass CPS Translation of Dependent Types (Talk Proposal)
12mOn the metatheory of IRs and the CPS-calculus
59mAn introduction to Continuation Passing Style (CPS)
15mCompiling with Continuations, Correctly
14mAdequacy for Algebraic Effects Revisited
18mWP-Preserving Compilation -- Preserving Weakest Preconditions For End-to-End Verification