Sébastien Carlier and J. B. Wells
Type inference with expansion variables
and intersection types in System E and an exact correspondence with
beta-reduction
In Proc. 6th Int'l Conf. Principles & Practice Declarative
Programming, 2004
Completely supersedes [?]
System E is a recently designed type system for the
lambda-calculus with intersection types and
expansion variables. During automatic type
inference, expansion variables allow postponing
decisions about which non-syntax-driven typing rules
to use until the right information is available and
allow implementing the choices via substitution.
This paper uses expansion variables in a
unification-based automatic type inference algorithm
for System E that succeeds for every
beta-normalizable lambda-term. We have
implemented and tested our algorithm and released
our implementation publicly. Each step of our
unification algorithm corresponds to exactly one
beta-reduction step, and vice versa. This
formally verifies and makes precise a step-for-step
correspondence between type inference and
beta-reduction. This also shows that type
inference with intersection types and expansion
variables can, in effect, carry out an arbitrary
amount of partial evaluation of the program being
analyzed.
[ 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.
