A new way of locating type errors is presented. It uses program slicing to improve the informativeness of error messages and the quality of the associated positional  information. 

The authors start with a framework in which type-checkers are specified algebraically and executed by a term rewriting system. In this model, a program’s abstract syntax tree is rewritten as a list of type errors. Each error message is associated with a slice of the program, which is achieved by using dependence tracking. To illustrate all this, the authors introduce a simple language, L. Some L programs are elaborately rewritten to error messages, using the specified rewrite rules.

The technique has been implemented using the ASF+SDF meta-environment, and has been tested on a subset of Pascal to which object-oriented type features, such as subtypes, have been added. Functional type systems can also be handled by this method, as the authors show for a subset of ML.

The paper is intended for everyone interested in language semantics and their implementation, and is easy to read. No prior knowledge of rewriting systems is needed; indeed, the paper might arouse interest in this topic. Adequate references are provided in that case.