Guarded Computational Type Theory

TL;DR

Guarded Computational Type Theory integrates Nakano's later modality with dependent types, enabling expressive recursive and productive programs while maintaining operational semantics and a hierarchy of universes.

Contribution

It introduces a novel clock intersection connective with clock irrelevance and a predicative universe hierarchy without clock context indexing.

Findings

Provides an operational account of guarded dependent type theory with clocks.

Features a new clock intersection connective with clock irrelevance.

Establishes a hierarchy of universes without clock context indexing.

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