Carnegie Mellon University
file.pdf (940.16 kB)

Inductively defined types in the Calculus of Constructions

Download (940.16 kB)
journal contribution
posted on 2008-07-01, 00:00 authored by Frank Pfenning, Christine Paulin-Mohring
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]."


Publisher Statement

© ACM, 2008. This is the author’s version of the work. It is posted here by permission of the ACM for your personal use. Not for redistribution. The definitive version was published in: Proc. of the 2008 International Conference on Image and Video Retrieval CIVR’08, July 7–9, 2008, Niagara Falls, Canada.



Usage metrics


    Ref. manager