Università di Torino

Research on "Formal Methods in Computing"

Principal Typings and True Rank 2 Intersection Typable Recursive Definitions

(suberseded by Rank 2 Intersection and Polymorphic Recursion )

Ferruccio DAMIANI

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.


   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/}

["Formal Methods in Computing" group] [Department's HOME]

Last update: Jan 20, 2005