Inductively defined types in the Calculus of Constructions

Abstract: "We define the notion of an inductively defined type in the Calculus of Constructions and show how inductively defined types can be represented by closed types. We show that all primitive recursive functionals over these inductively defined types are also representable. This generalizes work by Böhm & Berarducci on synthesis of functions on term algebras in the second-order polymorphic [lambda]-calculus (F [subscript 2]). We give several applications of this generalization, including representation of F [subscript 2]-programs in F [subscript 3], along with a definition of functions reify, reflect, and eval for F [subscript 2] in F [subscript 3]. We also show how to define induction over inductively defined types and sketch some results that show that the extension of the Calculus of Construction by induction principles does not alter the set of functions in its computational fragment, F [subscript omega]. This is because a proof by induction can be realized by primitive recursion, which is already definable in F [subscript omega]."