F. Damiani
Rank-2 intersection and
polymorphic recursion (extended version with proofs)
Internal report. Extended version with proofs
of [28], January 2005
Let |- be a rank-2 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
recursive definitions that are not simple.
At the best of our knowledge, previous algorithms for typing recursive
definitions in presence of intersection types allow only simple
recursive definitions to be typed. The proposed rules 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.
[ bib |
.pdf |
.html ]
Back
This file has been generated by
bibtex2html 1.43