Effectful Program Distancing

on YouTube ↗26m

" summary

Proposes a semantic framework that extends differential logical relations to effectful higher-order languages and proves a fundamental lemma that yields compositional reasoning about program distances. Builds a category of generalized distance spaces, models effects with monads and a differential extension of a monad (including distribution, writer, and cost monads), and defines ternary couplings for probabilistic liftings. Applies the method to loop perforation and approximate integration, gives concrete probabilistic distance bounds, and shows uses for cost analysis and differential privacy.

AI-written summary · about

" chapters (9)

1. 0:00Start
2. 5:06Approximate Computing
3. 6:58Loop Perforation
4. 8:42Differential Logical Relations
5. 10:40Generalized Distance Spaces
6. 11:49Exponential of Generalized System Spaces
7. 13:37What Is the Distance between Monolithic Values
8. 15:12Differential Extension of a Monument
9. 18:21Measure the Distance between Compound Systems