What makes guarded types tick?

Authors: Patrick Bahr, Bassel Mannaa and Rasmus Ejlers M√łgelberg

Paper Information

Title:What makes guarded types tick?
Authors:Patrick Bahr, Bassel Mannaa and Rasmus Ejlers M√łgelberg
Proceedings:PARIS Contributed papers
Editors: Alexis Saurin, David Baelde and Radu Calinescu
Keywords:Type Theory, Guarded Recursion, Reduction Semantics, Denotational Semantics

ABSTRACT. We give an overview of the syntax and semantics of Clocked Type Theory (CloTT), a dependent type theory for guarded recursion with many clocks, in which one can encode coinductive types and capture the notion of productivity in types. The main novelty of CloTT is the notion of ticks, which allows one to open the delay type modality, and, e.g., define a dependent form of applicative functor action, which can be used for reasoning about coinductive data. In the talk we will give examples of programming and reasoning about guarded recursive and coinductive data in CloTT, and we will present the main syntactic results: Strong normalisation, canonicity and decidability of type checking. If time permits, we will also sketch the main ideas of the denotational semantics for CloTT.

Talk:Jul 07 17:15 (Session 31L: Invited talk + contributed talk)