Inductive Data Type Systems: Strong Normalization
This paper is concerned with the
foundations of Inductive Data Type Systems, an extension of pure type
systems by inductive data types. IDTS generalize (inductive) types
equipped with primitive recursion of higher-type, by providing
definitions of functions by pattern matching following a generalized
form of the general recursive schema of Jouannaud and Okada, which
captures recursor definitions for arbitrary inductive types satisfying
the positivity condition. IDTS also generalize the first-order
framework of abstract data types by providing function types and
higher-order rewrite rules. The work is carried
out in the context of the simply typed lambda calculus, leaving its
generalization to richer calculi for future work.
full paper