Denotational Foundations for Expected Cost Analysis
summary
Introduces cert CBPV metalanguage and an operational cost semantics plus two denotational semantics: a distribution-over-(cost,output) cost semantics and an expected-cost monad pairing a nonnegative real expected cost with an output distribution. Proves operational soundness and adequacy for the cost semantics, a cost adequacy theorem for the expected-cost semantics, and an effect simulation property relating them; shows canonicity (minimality) and that for terminating programs expected costs coincide, and that the monad equals the fine fragment of the continuation monad in quasibel spaces.
AI-written summary · about
chapters (11)
- 0:00Expected cost analysis intro
- 1:02Limitations of cost semantics
- 2:48Distribution-based semantics problems
- 3:30CPS semantics issues
- 4:56Desired semantics properties
- 5:36Expected cost monad
- 7:21Geometric distribution example
- 9:29Advantages of expected cost semantics
- 10:37Relations to other semantics
- 11:41Monad general applicability
- 12:03Q&A
related talks
18mA modal type-theory of expected cost in higher-order probabilistic programs
49mSemantic Foundations for Probabilistic Programming
19mTowards Denotational Semantics of AD for Higher-Order, Recursive, Probabilistic
22mReasoning about 'Reasoning about Reasoning' Semantics and Contextual Equivalence
24mHigher order programming with probabilistic effects: A model of stochastic memo...
06mDistribution Theoretic Semantics for Non-Smooth Differentiable Programming
29mA Pre-Expectation Calculus for Probabilistic Sensitivity
01h 05mMonads in Modern C++