**You are here:**
» Intensional Type Theory with Guarded Recursive Types qua ...

## Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article

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 Grpdωop 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 |
---|

DOIs | |
---|

State | Published - 1 Jan 2013 |
---|

Event | Annual IEEE/ACM Symposium on Logic in Computer Science - New Orleans, United States Duration: 25 Jun 2013 → 28 Jan 2014 Conference number: 28 |
---|

Conference | Annual IEEE/ACM Symposium on Logic in Computer Science |
---|

Number | 28 |
---|

Country | United States |
---|

City | New Orleans |
---|

Period | 25/06/2013 → 28/01/2014 |
---|

Title of the vol.: 28th Annual IEEE/ACM Symposium on Logic in Computer Science (LICS), 2013 . ISBN: 978-1-4799-0413-6

See relations at Aarhus University
Citationformats

ID: 68846444