Assaf J. Kfoury, Geoff Washburn, and J. B. Wells
Implementing
compositional analysis using intersection types with expansion
variables
In Proceedings of the 2nd Workshop on Intersection Types and
Related Systems, 2002
A program analysis is compositional when the analysis
result for a particular program fragment is obtained solely from the
results for its immediate subfragments via some composition operator. This
means the subfragments can be analyzed independently in any order. Many
commonly used program analysis techniques (in particular, most abstract
interpretations and most uses of the Hindley/Milner type system) are not
compositional and require the entire text of a program for sound and
complete analysis. System I is a recent type system for the pure
lambda-calculus with intersection types and the new technology of
expansion variables. System I supports compositional analysis because it
has the principal typings property and an algorithm based on the new
technology of beta-unification has been developed that finds these
principal typings. In addition, for each natural number k, typability in
the rank-k restriction of System I is decidable, so a complete and
terminating analysis algorithm exists for the rank-k restriction.
This paper presents new understanding that has been gained from working
with multiple implementations of System I and beta-unification-based
analysis algorithms. The previous literature on System I presented the
type system in a way that helped in proving its more important theoretical
properties, but was not as easy for implementers to follow as it could be.
This paper provides a presentation of many aspects of System I that should
be clearer as well as a discussion of important implementation issues.
[ bib |
.pdf ]
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.
