ITU
ITU

What makes guarded types tick?

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

View graph of relations

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

Workshop

WorkshopProgramming And Reasoning on Infinite Structures
CountryUnited Kingdom
CityOxford
Period07/07/201808/07/2018

Downloads

No data available

ID: 83193671