|
J. B. Wells
The undecidability of Mitchell's subtyping
relation
Tech. Rep. 95-019, Comp. Sci. Dept., Boston Univ., December 1995
Mitchell defined and axiomatized a subtyping
relationship (also known as containment,
coercibility, or subsumption) over the
types of System F (with “->'' and
“for all''). This subtyping relationship is quite
simple and does not involve bounded
quantification. Tiuryn and Urzyczyn quite recently
proved this subtyping relationship to be
undecidable. This paper supplies a new
undecidability proof for this subtyping
relationship. First, a new syntax-directed
axiomatization of the subtyping relationship is
defined. Then, this axiomatization is used to prove
a reduction from the undecidable problem of
semi-unification to subtyping. The
undecidability of subtyping implies the
undecidability of type checking for System F
extended with Mitchell's subtyping, also known as
“F plus eta''.
[ bib |
.ps.gz |
.html ]
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.
|
