@inproceedings{nodelays,
  Title = {The Clocks Are Ticking: No More Delays!},
  Author = {Patrick Bahr and Hans Bugge Grathwohl and Rasmus Ejlers M\o{}gelberg},
  booktitle = {32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
  Month = jun,
  Year = {2017},
  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. 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.},
  Keywords = {type theory, guarded recursion, reduction semantics, strong normalisation,
                              coinductive types, recursive types},
  doi = {10.1109/LICS.2017.8005097},
  url = {http://ieeexplore.ieee.org/document/8005097/}
}