Marco Paviotti - Synthetic Guarded Domain Theory: Recursion in Guarded Recursion

Marco Paviotti, IT University of Copenhagen, Denmark

Title: "Synthetic Guarded Domain Theory: Recursion in Guarded Recursion”

Abstract: Guarded recursion is a form of recursion where recursive calls are guarded by delay modalities. Previous work has shown how guarded recursion is useful for constructing logics for reasoning about programming languages, as well as for constructing and reasoning about elements of co-inductive types. In this work I investigate how type theory with guarded recursion can be used as a metalanguage for denotational semantics for programming languages with (unguarded) recursion. More precisely, I construct a computationally adequate model for a lambda calculus with recursion (PCF) and for a lambda calculus with recursive types (FPC). These models are constructed using guarded recursion and therefore are rather intensional. I then show how to recover the usual extensional version of contextual equivalence by defining a logical relation. This work is related to Escardo’s metric model of PCF and to Pitts’s invariant relations, but here everything is carried out entirely in the type theory. This makes it easier to prove computational adequacy by logical relation argument. Joint work with Rasmus Møgelberg and Lars Birkedal.