@Article{ Ma2009.4,

author = {Matthes, Ralph},

title = "{An induction principle for nested datatypes in intensional type theory}",

journal = {Journal of Functional Programming},

publisher = {Cambridge University Press},

address = {http://www.cambridge.org/},

year = {2009},

month = {juin},

volume = {19},

number = {3&4},

pages = {439--468},

language = {anglais},

URL = {http://www.irit.fr/~Ralph.Matthes/works.html},

abstract = {Nested datatypes are families of datatypes that are indexed over all types such that the constructors may relate different family members (unlike the homogeneous lists). Moreover, the argument types of the constructors refer to indices given by expressions where the family name may occur. Especially in this case of true nesting, termination of functions that traverse these data structures is far from being obvious.
A joint article with A. Abel and T. Uustalu (TCS 333(1-2), pp. 3-66, 2005) proposes iteration schemes that guarantee termination not by structural requirements but just by polymorphic typing. They are generic in the sense that no specific syntactic form of the underlying datatype "functor" is required. However, there was no induction principle for the verification of the programs thus obtained although they are well-known in the usual model of initial algebras on endofunctor categories.
The new contribution is a representation of nested datatypes in intensional type theory (more specifically, in the Calculus of Inductive Constructions) that is still generic and covers true nesting, guarantees termination of all expressible programs and has an induction principle that allows to prove functoriality of monotonicity witnesses (maps for nested datatypes) and naturality properties of
iteratively defined polymorphic functions.}

}