The Clocks They Are Adjunctions: Denotational Semantics for Clocked Type Theory
Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review
for CloTT useful, e.g., for studying future extensions of CloTT with constructions such as path types.
The main challenge for constructing this model is to model the notion of ticks used in CloTT for coinductive reasoning about coinductive types. We build on a category previously used to model guarded recursion, but in this category there is no object of ticks, so tick-assumptions in a context can not be modelled using standard tools. Instead we show how ticks can be modelled using adjoint functors, and how to model the tick constant using a semantic substitution.
|Title of host publication||3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)|
|Number of pages||17|
|Publisher||Schloss Dagstuhl--Leibniz-Zentrum für Informatik|
|Publication status||Published - 2018|
|Event||International Conference on Formal Structures for Computation and Deduction - Oxford, United Kingdom|
Duration: 9 Jul 2018 → 12 Jul 2018
Conference number: 3
|Conference||International Conference on Formal Structures for Computation and Deduction|
|Periode||09/07/2018 → 12/07/2018|
|Series||Leibniz International Proceedings in Informatics (LIPIcs)|