^{1} Programming, Logic and Semantics, Software & Systems, The Department^{2} Theoretical Computer Science, The Department^{3} Programming Logic and Semantics, Theoretical Computer Science, The Department^{4} Computer Science, IT University of Copenhagen^{5} unknown

DOI:

10.1109/LICS.2013.27

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.

Type:

Journal article

Language:

English

Published in:

Annual Symposium on Logic in Computer Science, 2013, p. 213-222

Main Research Area:

Science/technology

Publication Status:

Published

Review type:

Peer Review

Conference:

Annual IEEE/ACM Symposium on Logic in Computer ScienceLogic in Computer Science, 2013