What makes guarded types tick?

Publikation: Konferencebidrag - EJ publiceret i proceeding eller tidsskriftPaperForskningpeer 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.
StatusUdgivet - 2018
BegivenhedProgramming And Reasoning on Infinite Structures - Oxford, Storbritannien
Varighed: 7 jul. 20188 jul. 2018


WorkshopProgramming And Reasoning on Infinite Structures


Dyk ned i forskningsemnerne om 'What makes guarded types tick?'. Sammen danner de et unikt fingeraftryk.