Clocked Type Theory

Clocked type theory (CloTT) is a system that extends Martin-Löf type theory with the notion of clocks. The aim is to produce a type theory for guarded recursion, which allows programing and reasoning with coinductive types, and allows productivity to be encoded in types.

References

CloTT was introduced in

Bahr, Patrick, Hans Bugge Grathwohl, and Rasmus Ejlers Møgelberg. 2017. ‘The Clocks Are Ticking: No More Delays!’ In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE. https://doi.org/10.1109/LICS.2017.8005097. pdf

@inproceedings{bahr_2017,
	title = {The clocks are ticking: {No} more delays!},
	url = {http://www.itu.dk/people/mogel/papers/lics2017.pdf},
	doi = {10.1109/LICS.2017.8005097},
	booktitle = {2017 32nd {Annual} {ACM}/{IEEE} {Symposium} on {Logic} in {Computer} {Science} ({LICS})},
	publisher = {IEEE},
	author = {Bahr, Patrick and Grathwohl, Hans Bugge and M{\o}gelberg, Rasmus Ejlers},
	year = {2017}
}

A denotational semantics for CloTT is given in

Mannaa, Bassel, Rasmus Ejlers Møgelberg, and Niccolò Veltri. n.d. ‘Ticking Clocks as Dependent Right Adjoints: Denotational Semantics for Clocked Type Theory’. Logical Methods in Computer Science 16 (4). https://doi.org/10.23638/LMCS-16(4:17)2020.

@article{mannaa_2020,
	title = {Ticking clocks as dependent right adjoints: {Denotational} semantics for clocked type theory},
	volume = {16},
  date = {2020},
	url = {https://lmcs.episciences.org/6980},
	doi = {10.23638/LMCS-16(4:17)2020},
	number = {4},
	journal = {Logical Methods in Computer Science},
	author = {Mannaa, Bassel and M{\o}gelberg, Rasmus Ejlers and Veltri, Niccol\`{o}},
}