|
Gang Chen
Coercive subtyping for
the calculus of constructions (extended abstract)
In Conf. Rec. POPL '03: 30th ACM Symp. Princ. of Prog. Langs., 2003
We present a coercive subtyping system for the calculus of
constructions. The proposed system lambda C<=co is obtained
essentially by adding coercions and eta-conversion to
lambda C<=[?], which is a subtyping
extension to the calculus of constructions without
coercions. Following [?], the coercive
subtyping c : A <= B is understood as a special case
of typing in arrow type c : A -> B such that the term
c behaves like an identity function. We prove that,
with respect to this semantic interpretation, the
proposed coercive subtyping system is sound and complete,
and that this completeness leads to transitivity
elimination. In addition, we establish the equivalence
between lambda C<=co and lambda Cbeta eta, this fact implies that
lambda C<=co has confluence, subject reduction and strong
normalization. We propose a formalization of coercion
inference problem and present a sound and complete
coercion inference algorithm.
[ bib |
.ps.gz |
.pdf.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.
|
