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