Rank 2 Types for Term Graph Rewriting

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 [5], a notion of principal pair which generalizes ML's principal type property.

• Type: Journal
• Year: 2002
• Where: ENTCS
• Authors: Steffen van Bakel
• Keywords: ENTCS 2002, Polymorphic Intersection Types, Term Graph, Type Assignment