Towards a Verified Cost Model for Call-by-Push-Value
summary
Claims a verified cost model for the call-by-push-value lambda-calculus mechanised in HOL4, by compiling CBPV terms into a substitution machine and proving a polynomial-time simulation relation to a low-level machine (hence reasonable relative to Turing machines). Prior call-by-value formalisation is ported to HOL4, the compiler and simulation lemmas are formalised, and the core simulation theorem shows k CBPV steps yield at most poly(k) machine steps; remaining work is extending to full CBPV features and client languages.
AI-written summary · about
chapters (4)
related talks
39mA Reusable Machine-Calculus for Automated Resource Analyses
18mA Simple and Efficient Implementation of Strong Call by Need by an Abstract Ma…
13mComputation Focusing
15mA Modular Cost Analysis for Probabilistic Programs
29mClosure Conversion in Little Pieces
26mTemporal refinements for Call-By-Push-Value with fixpoint
19mFormally Verifying Optimizations with Block Simulations
25mRelative Monads in CBPV for Stack-based Effects