## Abstract

Guarded recursive functions and types are useful

for giving semantics to advanced programming languages and

for higher-order programming with infinite data types, such

as streams, e.g., for modeling reactive systems.

We propose an extension of intensional type theory with

rules for forming fixed points of guarded recursive functions.

Guarded recursive types can be formed simply by taking fixed

points of guarded recursive functions on the universe of types.

Moreover, we present a general model construction for

constructing models of the intensional type theory with guarded

recursive functions and types. When applied to the groupoid

model of intensional type theory with the universe of small

discrete groupoids, the construction gives a model of guarded

recursion for which there is a one-to-one correspondence

between fixed points of functions on the universe of types and

fixed points of (suitable) operators on types.

In particular, we find that the functor category

from the preordered set of natural numbers to the category of

groupoids is a model of intensional type theory with guarded

recursive types.

for giving semantics to advanced programming languages and

for higher-order programming with infinite data types, such

as streams, e.g., for modeling reactive systems.

We propose an extension of intensional type theory with

rules for forming fixed points of guarded recursive functions.

Guarded recursive types can be formed simply by taking fixed

points of guarded recursive functions on the universe of types.

Moreover, we present a general model construction for

constructing models of the intensional type theory with guarded

recursive functions and types. When applied to the groupoid

model of intensional type theory with the universe of small

discrete groupoids, the construction gives a model of guarded

recursion for which there is a one-to-one correspondence

between fixed points of functions on the universe of types and

fixed points of (suitable) operators on types.

In particular, we find that the functor category

from the preordered set of natural numbers to the category of

groupoids is a model of intensional type theory with guarded

recursive types.

Original language | English |
---|---|

Journal | Annual Symposium on Logic in Computer Science |

Pages (from-to) | 213-222 |

Number of pages | 10 |

ISSN | 1043-6871 |

Publication status | Published - 2013 |