On the subject reduction property for algebraic type systems

Abstract

Algebraic type systems provide a general framework for the study of the interaction between typed λ-calculi and typed rewriting systems. A major problem in the development of a general theory for algebraic type systems is to prove that typing is preserved under reduction (Subject Reduction lemma). In this paper, we propose a general technique to prove Subject Reduction for a large class of algebraic type systems. The idea is to consider for every (functional) algebraic type system a labelled syntax for which Subject Reduction is easy to prove and then prove the equivalence between the labelled and standard syntaxes whenever the labelled system is strongly normalising. The equivalence can then be used to recover confluence, strong normalisation and subject reduction for the standard syntax.