Sébastien Carlier, Jeff Polakow, J. B. Wells, and A. J.
Kfoury
System E: Expansion variables for flexible
typing with linear and non-linear types and intersection types
In Programming Languages & Systems, 13th European Symp. Programming, volume 2986 of Lecture Notes in Computer Science, pages
294-309 Springer, 2004
Types are often used to control and analyze computer
programs. Intersection types give a type system
great flexibility, but have been difficult to
implement. The ! operator, used to distinguish
between linear and non-linear types, has good
potential for improving tracking of resource usage,
but has not been as flexible as one might want and
has been difficult to use in compositional
analysis. We introduce System E, a type system with
expansion variables, linear intersection types, and
the ! type constructor for creating non-linear
types. System E is designed for maximum flexibility
in automatic type inference and for ease of
automatic manipulation of type
information. Expansion variables allow postponing
the choice of which typing rules to use until later
constraint solving gives enough information to allow
making a good choice. System E removes many
limitations and technical difficulties that
expansion variables had in the earlier System I and
extends expansion variables to work with ! in
addition to the intersection type constructor. We
present subject reduction results for call-by-need
evaluation and discuss approaches for implementing
program analysis in System E.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43