Tags:clock irrelevance, clocks, dependent type, dependent type theory, dependent types, fixed point, forcing clause, guarded computational type theory, guarded dependent type theory, guarded recursion, inductive definition, internal logic, kripke joyal semantic, later modality, meaning explanation, modalities, operational semantic, presheaf topos, programming language, type system, type theory and universes

Abstract:

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 simple 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.