Aleš Bizjak: Guarded Dependent Type Theory: Syntax and Semantics

Aleš Bizjak, Aarhus University, Danska

Abstract:

Guarded dependent type theory is a version of (extensional) dependent type theory with a family of "later" modalities and "clocks" and clock quantifiers.

The later modalities are used for defining guarded recursive types, which are types where the type variable appears guarded by a "later" modality, but can otherwise appear positively or negatively or both, as well as to ensure productivity of (co)recursive definitions in a modular, type based, way.

Clocks and clock quantifiers are used for a controlled elimination of the later modalities and are used to get coinductive types from guarded recursive types.

In the first part of the talk I will present some of the new features of the
type theory (the new syntactic constructs) and show why they are needed with some examples.

In the second part I will present the basics of the model that is th inspiration behind the constructs and the rules of the type theory. 

Vabljeni!