Research on "Formal Methods in Computing"

Principal Typings and True Rank 2 Intersection Typable Recursive Definitions

(suberseded by Rank 2 Intersection and Polymorphic Recursion )

ABSTRACT. We propose new typing rules for assigning rank 2 intersection types to (possibly mutually) recursive definitions. A major achievement of the new rules over previous proposals is that they allow to type also true rank 2 intersection typable recursive definitions (i.e., recursive definitions that have a rank 2 intersection type and no simple type). A notable feature of these rules is that they rely entirely on principal typings, so they can be added to any system with principal typings.

• pdf

BIBTEX.

@techreport{Damiani:DART-2003,
   author      = {F. Damiani},
   title       = {Principal Typings and True Rank 2 Intersection 
		  Typable Recursive Definitions},
   year        = {2003},
   institution = {Part of Deliverable 2.3 of IST-2001-33477 (DART) project
	          - http://www.cee.hw.ac.uk/DART/}
}