F. Damiani
Rank 2 intersection types for
local definitions and conditional expressions
ACM Trans. on Prog. Langs. & Systs., 25(4):401-451,
2003
We introduce a rank 2 intersection type system
with new typing
rules for local definitions (LET-expressions and
LETREC-expressions) and conditional expressions
(IF-expressions and MATCH-expressions). This is a further
step towards the use of intersection types in ``real''
programming
languages.
The technique for typing local definitions relies entirely on
the
principal typing property (i.e. it does not depend on
particulars
of rank 2 typing), so it can be applied to any system with
principal typings. The technique for typing conditional
expressions, which is based on the idea of introducing metrics
on
types to ``limit the use'' of the intersection type
constructor in
the types assigned to the branches of the conditionals, is
instead
tailored to rank 2 intersection. However, the underlying idea
might be useful also for other type systems.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43