Abstract

We define a notion of type assignment with polymorphic intersection types of rank 2 for a term graph rewriting language that expresses sharing and cycles. We show that type assignment is decidable through defining, using the extended notion of unification from [Bakel-Barbanera-Fernandez-Types'00], a notion of principal pair which generalizes ML's principal type property.

Appeared as:

@Inproceedings{Bakel-TIP'02,

Author = "S. van Bakel",
Title = "{R}ank 2 {T}ypes for {T}erm {G}raph {R}ewriting ({E}xtended {A}bstract)",
Booktitle = "Electronic Proceedings of International Workshop {\em Types in Programming} (TIP'02), Dagstuhl, Germany",
Series = "Electronic Notes in Theoretical Computer Science",
Volume = "75",
Year = "2002",
Note = "http://www.elsevier.nl/locate/entcs/volume75.html"
}