Abstract Data Type Systems
This paper is concerned with the foundations of an
extension of pure type systems by abstract data types, hence the name
of Abstract Data Type Systems. ADTS generalize inductive types
as they are defined in the calculus of
constructions, by providing definitions of
functions by pattern matching on one hand, and relations among
constructors of the inductive type on the other hand. It also
generalizes the first-order framework of abstract data types by
providing function types and higher-order equations. The first half of
the paper describes the framework of ADTS, while the second half
investigates cases where ADTS are strongly normalizing. This is shown
to be the case for the polymorphic lambda calculus (with possibly
subtypes) enriched by higher-order algebraic rules obeying a strong
generalization of primitive recursion of higher type that we call the
{\em general schema}. This covers in particular the case of inductive
types whose constructors do not have functional arguments. We
conjecture that this result holds true for all calculi of the so called
Barendregt's cube. On the other hand, the definition of a schema for
the higher-order rules allowing for more general inductive types is left
open.
full paper