Abstract

In this paper we define and study intersection type assignment systems for first-order rewriting extended with application, lambda-abstraction, and beta-reduction (TRS + beta). One of the main results presented is that, using a suitable notion of approximation of terms, any typeable term of a TRS + beta that satisfies a general scheme for recursive definitions has an approximant of the same type. From this result we deduce, for different classes of typeable terms, a head-normalization and a normalization theorem.

Appeared in:

@Inproceedings {Bakel-Barbanera-Fernandez-ESOP'96,

Author = "S. van Bakel and F. Barbanera and M. Fern\'andez",
Title = "{R}ewrite {S}ystems with {A}bstraction and $\beta$-rule: {T}ypes, {A}pproximants and {N}ormalization",
Booktitle = "Programming Languages and Systems -- ESOP'96. Proceedings of 6th European Symposium on Programming, {\rm Link{\"o}ping, Sweden}",
Editor = "Hanne Riis Nielson",
Series = "Lecture Notes in Computer Science",
Volume = "1058",
Publisher = "Springer-Verlag",
Year = "1996",
Pages = "387-403"
}