Guarded Dependent Type Theory with Coinductive Types

TL;DR

This paper introduces guarded dependent type theory (gDTT), an extension of dependent type theory with modalities and clock quantifiers to support productive recursive and coinductive types, enabling modular programming and proofs.

Contribution

It develops novel delayed substitution mechanisms and demonstrates the soundness of gDTT with respect to a denotational model, advancing the theory of guarded recursion.

Findings

Soundness of gDTT established

Novel delayed substitution formers introduced

Encoding of coinductive types using guarded recursion

Abstract

We present guarded dependent type theory, gDTT, an extensional dependent type theory with a `later' modality and clock quantifiers for programming and proving with guarded recursive and coinductive types. The later modality is used to ensure the productivity of recursive definitions in a modular, type based, way. Clock quantifiers are used for controlled elimination of the later modality and for encoding coinductive types using guarded recursive types. Key to the development of gDTT are novel type and term formers involving what we call `delayed substitutions'. These generalise the applicative functor rules for the later modality considered in earlier work, and are crucial for programming and proving with dependent types. We show soundness of the type theory with respect to a denotational model.