An introduction to synthetic guarded domain theory with applications to probabilistic(…)
summary
Presents a clocked cubical type theory metalanguage that uses a guarded delay monad to define both big‑step operational and denotational semantics for FPC and FPC with probabilistic choice, builds an evaluation function and a guarded logical relation, and proves computational adequacy (denotational equality implies contextual equivalence). Models probabilistic choice as a free convex algebra / finite distribution HIT, proves examples: hesitant identity equals id, unfair‑coin → fair‑coin simulator, and a two‑step vs one‑step random walk equivalence; approach extends to higher‑order store and is implementable in Cubical Agda.
AI-written summary · about
chapters (17)
- 0:00Synthetic guarded domain theory intro
- 7:00Talk overview and literature
- 9:33Clock cubical type theory with GED recursion
- 15:52Topos of trees and guarded recursion
- 22:38Reasoning with guarded recursion example
- 27:40Modeling FPC via guarded recursion
- 36:10Computational adequacy and logical relations
- 37:35Q&A after FPC modeling
- 37:57Extending FPC with probabilistic choice
- 41:52Contextual equivalence for probabilistic FPC
- 45:25Guarded recursion with probabilistic choice
- 48:14Termination probability in probabilistic FPC
- 51:04Semantics for probabilistic FPC
- 53:34Lifting relations for probabilistic computations
- 55:00Reasoning examples with probabilistic FPC
- 56:23Conclusion and extensions
- 57:03Q&A
related talks
25mFormalizing pi-Calculus in Guarded Cubical Agda
49mSemantic Foundations for Probabilistic Programming
22mAlgebraic Effects Meet Hoare Logic in Cubical Agda
26mTemporal refinements for Call-By-Push-Value with fixpoint
24mAn Intrinsically-typed Probabilistic Programming Language in Coq (Extended Abstr...
30mPlausible sealing for gradual parametricity
24mA Computational Interpretation of Compact Closed Categories
25mCubical Synthetic Homotopy Theory