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.