Modelling Recursion and Probabilistic Choice in Guarded Type Theory

on YouTube ↗18m

" summary

Paper encodes FPC⊕ (recursive types + probabilistic choice) inside clocked guarded type theory and builds operational and denotational semantics connected by a logical relation that yields adequacy and contextual equivalence. Key constructions are a guarded convex delay monad (later/next guarded recursion gives a genuine fixed point), higher inductive finite distributions, and a lifting via couplings. Concrete results: a proof that the hesitant identity is contextually equivalent to identity and that the fair coin encoding from a biased coin preserves distribution.

AI-written summary · about

" chapters (10)

1. 0:00Probabilistic programming in guarded type theory
2. 0:50Recursion and probabilistic choice challenges
3. 2:34Guarded recursion in clock cubical type theory
4. 4:41Recursion with convex delay monad
5. 6:27Guarded convex delay monad
6. 8:15Semantics of probabilistic FPC with guarded recursion
7. 10:47Logical relations for program equivalence
8. 12:11Equivalence of hesitant identity function
9. 13:58Conclusion
10. 14:46Q&A