Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory

Bassel Mannaa, Rasmus Ejlers Møgelberg, Niccolò Veltri

Clocked Type Theory (CloTT) is a type theory for guarded recursion useful for programming with coinductive types, allowing productivity to be encoded in types, and for reasoning ab…