  Nakano's later modality can be used to specify and define recursive functions
which are causal or synchronous; in concert with a notion of clock variable, it
is possible to also capture the broader class of productive (co)programs. Until
now, it has been difficult to combine these constructs with dependent types in
a way that preserves the operational meaning of type theory and admits a
hierarchy of universes. We present an operational account of guarded dependent
type theory with clocks called Guarded Computational Type Theory, featuring a
novel clock intersection connective that enjoys the clock irrelevance
principle, as well as a predicative hierarchy of universes which does not
require any indexing in clock contexts. Guarded Computational Type Theory is
simultaneously a programming language with a rich specification logic, as well
as a computational metalanguage that can be used to develop semantics of other
languages and logics.
