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

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

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 languageEnglish
JournalAnnual Symposium on Logic in Computer Science
Pages (from-to)213-222
Number of pages10
ISSN1043-6871
DOIs
StatePublished - 1 Jan 2013
EventAnnual IEEE/ACM Symposium on Logic in Computer Science - New Orleans, United States
Duration: 25 Jun 201328 Jan 2014
Conference number: 28

Conference

ConferenceAnnual IEEE/ACM Symposium on Logic in Computer Science
Number28
CountryUnited States
CityNew Orleans
Period25/06/201328/01/2014

Bibliographical note

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