A modal type-theory of expected cost in higher-order probabilistic programs
summary
pλ-amor is a graded modal type theory that encodes probabilities, potentials and expected cost at the type level and proves bounds for higher-order probabilistic recursion. It gives RWM a type that records a logarithmic expected-mistake bound (log Σ_t / η) using a potential modality, implements cost as a PC monad with a tick construct, uses probabilistic couplings to avoid convolution, and proves soundness via a Kripke step-indexed model relating static potentials and runtime distributions.
AI-written summary · about
chapters (11)
- 0:00Expected cost analysis intro
- 1:28Experts problem algorithm
- 3:57Potential functions for bounds
- 6:27PλMR type theory
- 7:31Graded modalities in PλMR
- 9:38Cost modeling with tick
- 11:26Probabilistic couplings
- 13:14Potential modality operations
- 15:21Relating cost and potential
- 16:47Semantic model and soundness
- 17:52Additional modalities examples
related talks
13mDenotational Foundations for Expected Cost Analysis
24mHigher order programming with probabilistic effects: A model of stochastic memo...
59mA Welcome to Causal Probabilistic Programming
13mTyped Abstractions for Causal Probabilistic Programming
49mSemantic Foundations for Probabilistic Programming
29mMotivating Probabilistic Programming
19mTowards Denotational Semantics of AD for Higher-Order, Recursive, Probabilistic
12mLanguage-Model Probabilistic Programming for Improving Autoformalization via Cycle(…)