Publication: Research › Ph.D. thesis

In this dissertation we study applications and semantics of guarded recursion, which is a method for ensuring that self-referential descriptions of objects define a unique object.

The first two chapters are devoted to applications.

We use guarded recursion, first in the form of explicit step-indexing and then in the form of the internal language of particular sheaf topos, to construct logical relations for reasoning about contextual approximation of probabilistic and nondeterministic programs.

These logical relations are sound and complete and useful for showing a range of example equivalences.

In the third chapter we study a simply typed calculus with additional "later" and "constant" modalities and a guarded fixed-point combinator.

These are used for encoding and working with guarded recursive and coinductive types in a modular way.

We develop a normalising operational semantics, provide an adequate denotational model and a logic for reasoning about program equivalence.

In the last three chapters we study syntax and semantics of a dependent type theory with a family of later modalities indexed by the set of clocks, and clock quantifiers.

In the fourth and fifth chapters we provide two model constructions, one using a family of presheaf categories and one using a generalisation of the category of partial equilogical spaces.

These model constructions are used to design the rules and prove consistency of the type theory presented in the last chapter.

The type theory is a version of polymorphic dependent type theory with one kind, the kind of clocks, and a family of universes.

The modalities and clock quantifiers are used for defining coinductive types and functions on them.

The type theory is interesting because the guardedness condition, ensuring that (co)recursive definitions define unique objects, is expressed using types, in contrast to a syntactic guardedness condition.

This allows for a modular treatment of (co)recursive definitions.

The first two chapters are devoted to applications.

We use guarded recursion, first in the form of explicit step-indexing and then in the form of the internal language of particular sheaf topos, to construct logical relations for reasoning about contextual approximation of probabilistic and nondeterministic programs.

These logical relations are sound and complete and useful for showing a range of example equivalences.

In the third chapter we study a simply typed calculus with additional "later" and "constant" modalities and a guarded fixed-point combinator.

These are used for encoding and working with guarded recursive and coinductive types in a modular way.

We develop a normalising operational semantics, provide an adequate denotational model and a logic for reasoning about program equivalence.

In the last three chapters we study syntax and semantics of a dependent type theory with a family of later modalities indexed by the set of clocks, and clock quantifiers.

In the fourth and fifth chapters we provide two model constructions, one using a family of presheaf categories and one using a generalisation of the category of partial equilogical spaces.

These model constructions are used to design the rules and prove consistency of the type theory presented in the last chapter.

The type theory is a version of polymorphic dependent type theory with one kind, the kind of clocks, and a family of universes.

The modalities and clock quantifiers are used for defining coinductive types and functions on them.

The type theory is interesting because the guardedness condition, ensuring that (co)recursive definitions define unique objects, is expressed using types, in contrast to a syntactic guardedness condition.

This allows for a modular treatment of (co)recursive definitions.

Original language | English |
---|

Number of pages | 305 |
---|---|

State | Published - 15 Apr 2016 |

See relations at Aarhus University Citationformats

ID: 96256581