The Clocks Are Ticking: No More Delays! Reduction Semantics for Type Theory with Guarded Recursion

Patrick Bahr, Hans Bugge Grathwohl, Rasmus Ejlers Møgelberg

Research output: Journal Article or Conference Article in JournalConference articleResearchpeer-review


Guarded recursion in the sense of Nakano allows general recursive types and terms to be added to type theory without breaking consistency. Recent work has demonstrated applications of guarded recursion such as programming with codata, reasoning about coinductive types, as well as constructing and reasoning about denotational models of general recursive types. Guarded recursion can also be used as an abstract form of step-indexing for reasoning about programming languages with advanced features. Ultimately, we would like to have an implementation of a type theory with guarded recursion in which all these applications can be carried out and machine-checked. In this paper, we take a step towards this goal by devising a suitable reduction semantics. We present Clocked Type Theory, a new type theory for guarded recursion that is more suitable for reduction semantics than the existing ones. We prove confluence, strong normalisation and canonicity for its reduction semantics, constructing the theoretical basis for a future implementation. We show how coinductive types as exemplified by streams can be encoded, and derive that the type system ensures productivity of stream definitions.
Original languageEnglish
JournalAnnual Symposium on Logic in Computer Science
Number of pages12
Publication statusPublished - 18 Aug 2017
EventThirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science - Reykjavik, Iceland
Duration: 20 Jun 201723 Aug 2017
Conference number: 32


ConferenceThirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science


  • type theory, guarded recursion, reduction semantics, strong normalisation, coinductive types, recursive types

Cite this