Inductive Definition in Type Theory

Other Titles


Type theories can provide a foundational account of constructive mathematics, and for the computer scientist, they can also serve the dual roles of specification and programming languages. In the search for natural and expressive extensions to the NuPrl type theory, we are lead to consider forms of inductive and co-inductive definition. We realize these notions through the addition of two new type constructors, denoted μandν. This represents a step towards a more expressive theory, without adopting a completely impredicative notion of type. With these constructors we can define all the common inductive data types, from natural numbers to infinite trees. Through the propositions-as-types principle, these type constructors yield inductively defined propositions. The induction principle associated with the μ types lets us define well-founded recursive functions, and dual principle for the ν types lets us inductively define their "infinite" elements. We present another induction principle for the μ types which takes advantage of the information hiding properties of the Missing open brace for subscript\{ __ | __ \}\{ __ | __ \} type, and can be used to define an unbounded search operator, or more generally, to compute not with elements of the μ type, but under the assumption of its inhabitation. After presenting the proof rules for these new type constructors we give a semantic account, from which intuitionistic consistency is a consequence. First, we consider the the question of inductive types in the simpler setting of the second-order lambda calculus, where we prove a strong normalization property. We also consider typing terms in the presence of type constraints, and present a condition on the constraints (of polynomial complexity in the size of the constraints) for determining if the terms will be strongly normalizable or there will be a diverging typed term. Second, we develop a semantic account of the basic type theory, then relativize it to account for the impredicativity inherent in the definition of the new type constructors. We also show how this model can justify other impredicative type constructors, such as an impredicative type abstraction operation.

Journal / Series

Volume & Issue



Date Issued



Cornell University


computer science; technical report


Effective Date

Expiration Date




Union Local


Number of Workers

Committee Chair

Committee Co-Chair

Committee Member

Degree Discipline

Degree Name

Degree Level

Related Version

Related DOI

Related To

Related Part

Based on Related Item

Has Other Format(s)

Part of Related Item

Related To

Related Publication(s)

Link(s) to Related Publication(s)


Link(s) to Reference(s)

Previously Published As

Government Document




Other Identifiers


Rights URI


technical report

Accessibility Feature

Accessibility Hazard

Accessibility Summary

Link(s) to Catalog Record