
DIPARTIMENTO DI INFORMATICA Università di Torino

Research on "Formal Methods in Computing"

Rank 2 intersection types for local definitions and conditional expressions

(Supersedes the paper [Damiani, 2005] )

Ferruccio DAMIANI

ABSTRACT. Let |- be an intersection type system. We say that a term is |-simple (or just simple when the system |- is clear from the context) if system |- can prove that it has a simple type. In this paper we propose new typing rules and algorithms that are able to type (with rank~2 intersection types) recursive definitions that are not simple. Typing rules for assigning intersection types to (non-simple) recursive definitions have been already proposed in the literature. However, at the best of our knowledge, previous algorithms for typing recursive definitions in the presence of intersection types allow only simple recursive definitions to be typed. The rules and algorithms proposed in this paper are also able to type interesting examples of polymorphic recursion (i.e., recursive definitions rec {x=e} where different occurrences of x in e are used with different types). Moreover, the underlying techniques do not depend on particulars of rank~2 intersection, so they can be applied to other type systems.
An on-line demostration of a prototype implementation of the type system presented in the paper is available.

The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.

BIBTEX.

@article{tipoA-Damiani:FI-07,
  number = {4},
  volume = {77},
  author = {Ferruccio Damiani},
  url = {http://www.di.unito.it/~damiani/papers/fi1.html},
  tag = {Fundamenta Informaticae, 77},
  title = {Rank 2 Intersection for Recursive Definitions},
  publisher = {IOS Press},
  journal = {Fundamenta Informaticae},
  year = {2007},
  pages = {451-488},
}

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


	Last update: Mar 16, 2007