What makes guarded types tick?

Research output: Contribution to conference - NOT published in proceeding or journalPaperResearchpeer-review


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.
Original languageEnglish
Publication date2018
Publication statusPublished - 2018
EventProgramming And Reasoning on Infinite Structures - Oxford, United Kingdom
Duration: 7 Jul 20188 Jul 2018


WorkshopProgramming And Reasoning on Infinite Structures
Country/TerritoryUnited Kingdom


  • Clocked Type Theory
  • Guarded Recursion
  • Coinductive Types
  • Productivity in Types
  • Dependent Type Theory


Dive into the research topics of 'What makes guarded types tick?'. Together they form a unique fingerprint.

Cite this