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 [49]
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.43