Abstract

In this paper we study normalization properties of rewrite systems that are typeable using intersection types with omega and with sorts. We prove two normalization properties of typeable systems. On one hand, for all systems that satisfy a variant of the Jouannaud-Okada Recursion Scheme, every term typeable with a type that is not omega is head normalizable. On the other hand, non-Curryfied terms that are typeable with a type that does not contain omega, are normalizable.

Appeared as:

@Inproceedings {Bakel-Fernandez-RTA'95,

Author = "S. van Bakel and M. Fern\'andez",
Title = "({H}ead-){N}ormalization of {T}ypeable {R}ewrite {S}ystems",
Booktitle = "Proceedings of RTA '95. 6th International Conference on Rewriting Techniques and Applications, {\rm Kaiserslautern, Germany}",
Editor = "Jieh Hsiang",
Series = "Lecture Notes in Computer Science",
Volume = "914",
Publisher = "Springer-Verlag",
Year = "1995",
Pages = "279-293"
}