####
Termination of Algebraic Type Systems:

the Syntactic Approach

For several purposes it is useful to consider a
combination of a type theory (a typed lambda
calculus) and rewriting, for instance for program
transformation and proof checking.
A natural question is whether the combination of a
terminating type theory and a terminating rewriting
system is again terminating, where termination means
that there are no infinite computations.
The proofs that have been given so far (in various
different settings) consist basically in redoing
the termination proof for the type theory, which is
usually very difficult.

We consider a general framework to study combinations
of type theory and rewriting, the algebraic type systems,
and provide two general methods to derive termination
of the combination of a type theory and a rewriting
system from termination of those systems separately.