The Clocks Are Ticking: No More Delays!

Abstract

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. As a step towards an implementation of a type theory with guarded recursion, 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.

Category: Type Systems

Tags: Type Theory, Guarded Recursion, Reduction Semantics, Strong Normalisation, Coinductive Types, Recursive Types