Inductively defined types in the Calculus of Constructions Export

@incollection{citeulike:5433078, 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 Bhm \& Berarducci on synthesis of functions on term algebras in the second-order polymorphic λ-calculus (F 2). We give several applications of this generalization, including a representation of F 2-programs in F 3, along with a definition of functions reify, reflect, and eval for F 2 in F 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 ω. This is because a proof by induction can be realized by primitive recursion, which is already definable in F ω.}, author = {Pfenning, Frank and Paulin-Mohring, Christine}, citeulike-article-id = {5433078}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/BFb0040259}, citeulike-linkout-1 = {http://www.springerlink.com/content/t620126624802470}, doi = {10.1007/BFb0040259}, journal = {Mathematical Foundations of Programming Semantics}, pages = {209--228}, posted-at = {2009-08-13 18:59:49}, priority = {2}, title = {Inductively defined types in the Calculus of Constructions}, url = {http://dx.doi.org/10.1007/BFb0040259}, year = {1990} }

TY - CHAP ID - citeulike:5433078 L3 - citeulike-article-id:5433078 N2 - 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 Bhm & Berarducci on synthesis of functions on term algebras in the second-order polymorphic λ-calculus (F 2). We give several applications of this generalization, including a representation of F 2-programs in F 3, along with a definition of functions reify, reflect, and eval for F 2 in F 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 ω. This is because a proof by induction can be realized by primitive recursion, which is already definable in F ω. JF - Mathematical Foundations of Programming Semantics EP - 228 TI - Inductively defined types in the Calculus of Constructions SP - 209 AU - Pfenning, Frank AU - Paulin-Mohring, Christine PY - 1990/// UR - http://dx.doi.org/10.1007/BFb0040259 ER -