Guarded recursion is a type based approach to recursion in which the circularities of recursive definitions are broken using a modality for time steps. In this talk I will show how a type theory with guarded recursion can be used as a metalanguage for both denotational and operational semantics, a programme often referred to as synthetic guarded domain theory. When doing this, guarded recursion is used in all steps of the process: Defining the semantics, reasoning about the semantics (for example when proving adequacy), and for reasoning about programs.

I will illustrate the ideas in two examples. The first is the language FPC, a call-by-value lambda calculus with recursive types. The second is an extension of FPC with finite probabilistic choice. The talk will include an introduction to guarded recursion.

The talk is based on a recent preprint: P. J. A. Stassen, R. E. Møgelberg, M. Zwart, A. Aguirre, and L. Birkedal. Modelling probabilistic FPC in guarded type theory. arXiv:2408.04455, 2024. as well as previous joint work with Marco Paviotti.