|
Adam Bakewell, Sébastien Carlier, A. J. Kfoury, and J. B.
Wells
Inferring
intersection typings that are equivalent to call-by-name and call-by-value
evaluations
Technical report, Church Project, Boston University, April 2005
We present a procedure to infer a typing for an
arbitrary lambda-term M in an intersection-type
system that translates into exactly the call-by-name
(resp., call-by-value) evaluation of M. Our
framework is the recently developed System E which
augments intersection types with expansion
variables. The inferred typing for M is obtained
by setting up a unification problem involving both
type variables and expansion variables, which we
solve with a confluent rewrite system. The inference
procedure is compositional in the sense that
typings for different program components can be
inferred in any order, and without knowledge
of the definition of other program components.
Using expansion variables lets us achieve a
compositional inference procedure
easily. Termination of the procedure is generally
undecidable. The procedure terminates and returns a
typing iff the input M is normalizing according to
call-by-name (resp., call-by-value). The inferred
typing is exact in the sense that the exact
call-by-name (resp., call-by-value) behaviour of M
can be obtained by a (polynomial) transformation of
the typing. The inferred typing is also
principal in the sense that any other typing
that translates the call-by-name (resp.,
call-by-value) evaluation of M can be obtained
from the inferred typing for M using a
substitution-based transformation.
[ bib |
.ps.gz |
.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.
|
