Safe Couplings: Coupled Refinement Types
summary
Enhances refinement types with a coupling-based connective that captures relational properties like expected sensitivity and proves that output-distance is upper-bounded by an input-distance times a computable constant; implements the system inside Liquid Haskell and mechanizes proofs for two real algorithms, TD reinforcement learning and stochastic gradient descent. Builds a discrete-distribution semantics and proves soundness of the fragment, provides artifacts (code and proofs), and reports much smaller, more direct relational proofs compared to one-sided encodings.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:55Presentation
- 1:23Defining a probabilistic program
- 3:07Do notation
- 4:08Relational types
- 7:37Verification in Haskell
- 11:00Stochastic Descent Gradient
- 12:58Examples
- 14:03Paper
- 14:33Conclusion
related talks
40mType-Driven Program Synthesis
48mSpatial Coupling as a Proof Technique
29mA Pre-Expectation Calculus for Probabilistic Sensitivity
01h 12mTruth about Types
23mA Framework of Differential Operators
49mSemantic Foundations for Probabilistic Programming
06mLightning Talk: Curry-Howard Correspondence
06mDistribution Theoretic Semantics for Non-Smooth Differentiable Programming