|
Sébastien Carlier
Polar type inference with intersection types and
omega
In Proceedings of the 2nd Workshop on Intersection Types and
Related Systems, 2002
We present a type system featuring intersection
types and omega, a type constant which is
assigned to unused terms. We exploit and extend the
technology of expansion variables from the recently
developed System I, with which we believe our system
shares many interesting properties, such as strong
normalization, principal typings, and compositional
analysis. Our presentation emphasizes a polarity
discipline and shows its benefits. We syntactically
distinguish positive and negative types, and give
them different interpretations. We take the point of
view that the interpretation of a type is intrinsic
to it, and should not change implicitly when it
appears at the opposite polarity. Our system is the
result of a process which started with an extension
of Trevor Jim's Polar Type System.
[ bib |
.ps.gz ]
Back
This file has been generated by
bibtex2html 1.61
Copyright notice: The documents contained
in these pages are included by the contributing authors as a means to
ensure timely dissemination of scholarly and technical work on a
non-commercial 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.
If you experience problems downloading any of the files above,
it is most likely because your browser does not handle compressed
files correctly.
In particular, Netscape might save the file in the compressed
gz-format with extension .ps or
.pdf (indicating postscript or PDF, resp.). You can work around this by saving the file,
renaming it to .ps.gz or .pdf.gz, and then
uncrompress it.
|
