Abstract

We define two type assignment systems for first-order rewriting extended with application, λ-abstraction, and β-reduction. The types used in these systems are a combination of (omega-free) intersection and polymorphic types. The first system is the general one, for which we prove a subject reduction theorem and show that all typeable terms are strongly normalisable. The second is a decidable subsystem of the first, by restricting types to Rank 2. For this system we define, using an extended notion of unification, a notion of principal type, and show that type assignment is decidable.

Appeared in

@Inproceedings {Bakel-Barbanera-Fernandez-Types'00,

Author ="S. van Bakel and F. Barbanera and M. Fern\'andez",
Title = "Polymorphic {I}ntersection {T}ype {A}ssignment for {R}ewrite {S}ystems with {A}bstraction and $\beta$-rule",
Booktitle = "Types for Proofs and Programs. International Workshop, TYPES'99, {\rm L{\"o}keberg, Sweden, Sected Papers}",
Editor = "Thierry Coquand, Peter Dybjer, Bengt Nordstr{\"o}m, Jan Smith",
Series = "Lecture Notes in Computer Science",
Volume = "1956",
Publisher = "Springer-Verlag",
Year = "2000",
Pages = "41-60"
}