Projects per year
Abstract
We present a new model of guarded dependent type theory (GDTT), a type theory with guarded recursion and multiple clocks in which one can program with and reason about coinductive types. Productivity of recursively defined coinductive programs and proofs is encoded in types using guarded recursion and can
therefore be checked modularly, unlike the syntactic checks implemented in modern proof assistants. The model is based on a category of covariant presheaves over a category of time objects, and quantification over clocks is modelled using a presheaf of clocks. To model the clock irrelevance axiom, crucial for programming with coinductive types, types must be interpreted as presheaves internally right orthogonal to the object of clocks. In the case of dependent types, this translates to a lifting condition similar to the one
found in homotopy theoreticmodels of type theory, but here with an additional requirement of uniqueness of lifts. Since the universes defined by the standard Hofmann–Streicher construction in this model do not satisfy this property, the universes in GDTT must be indexed by contexts of clock variables. We show how
to model these universes in such a way that inclusions of clock contexts give rise to inclusions of universes commuting with type operations on the nose.
therefore be checked modularly, unlike the syntactic checks implemented in modern proof assistants. The model is based on a category of covariant presheaves over a category of time objects, and quantification over clocks is modelled using a presheaf of clocks. To model the clock irrelevance axiom, crucial for programming with coinductive types, types must be interpreted as presheaves internally right orthogonal to the object of clocks. In the case of dependent types, this translates to a lifting condition similar to the one
found in homotopy theoreticmodels of type theory, but here with an additional requirement of uniqueness of lifts. Since the universes defined by the standard Hofmann–Streicher construction in this model do not satisfy this property, the universes in GDTT must be indexed by contexts of clock variables. We show how
to model these universes in such a way that inclusions of clock contexts give rise to inclusions of universes commuting with type operations on the nose.
Original language  English 

Journal  Mathematical Structures in Computer Science 
Volume  30 
Issue number  4 
Pages (fromto)  342378 
ISSN  09601295 
DOIs  
Publication status  Published  Apr 2020 
Keywords
 Type theory
 denotational semantics
 guarded recursion
 coinductive types
Fingerprint
Dive into the research topics of 'Denotational semantics for guarded dependent type theory'. Together they form a unique fingerprint.Projects
 2 Finished

Type theories for reactive programming
Møgelberg, R. E. (PI), Vezzosi, A. (CoI), Graulund, C. U. (CoI), Kristensen, M. B. (CoI) & Veltri, N. (CoI)
22/01/2016 → 21/01/2022
Project: Research

Guarded recursive types in the foundations of programming
Møgelberg, R. E. (PI), Mannaa, B. (CoI) & Bahr, P. (CoI)
Independent Research Fund Denmark
01/07/2015 → 31/01/2019
Project: Research