Guarded Computational Type Theory

Authors: Jonathan Sterling and Robert Harper

Paper Information

Title:Guarded Computational Type Theory
Authors:Jonathan Sterling and Robert Harper
Proceedings:LICS PDF files
Editors: Anuj Dawar and Erich Grädel
Keywords:type theory, guarded recursion, clocks, dependent types, universes, modalities

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.

Talk:Jul 10 11:20 (Session 54E)