Modelling Recursion and Probabilistic Choice in Guarded Type Theory

Watch this 18-minute conference talk from POPL 2025 that explores how to define and reason about FPC⊕, a programming language with probabilistic choice and recursive types, within guarded type theory. Learn how researchers from Aarhus University and IT University of Copenhagen use higher inductive types to represent finite distributions and guarded recursion to model recursion. The presentation demonstrates both operational and denotational semantics of FPC⊕ and explains the relation between them, which can be used to prove adequacy and reason about programs up to contextual equivalence. Discover how this approach addresses the challenges of extending constructive type theory to languages with recursion and computational effects like probabilistic choice.