Inductive Data Type Systems
In a previous work (``Abstract Data Type Systems'', TCS
173(2):349--391 (1997)), the last two authors presented a combined
language made of a (strongly normalizable) algebraic rewriting system,
and a typed $\lambda$-calculus enriched by pattern-matching
definitions following a certain format, called the ``General Schema'',
which generalizes the usual recursor definitions for the natural
numbers and similar ``basic inductive types''. This combined language
was shown to be strongly normalizable. The purpose of this paper is
to extend the General Schema in order to capture a more general class
of inductive types, called ``strictly positive inductive types'', and
to prove the strong normalizability of the resulting combined system.
This result provides the computation model for the combined language
of an algebraic specification language based on abstract data types,
and the strongly typed functional language with strictly positive
inductive types.
full paper
full paper