|
A. J. Kfoury and J. B. Wells
New notions of reduction and non-semantic proofs of beta-strong
normalization in typed lambda-calculi
In Proc. 10th Ann. IEEE Symp. Logic in Comput. Sci., pages
311-321, 1995
Two notions of reduction for terms of the
lambda-calculus are introduced and the question
of whether a lambda-term is beta-strongly
normalizing is reduced to the question of whether a
lambda-term is merely normalizing under one of
the notions of reduction. This gives a method to
prove strong beta-normalization for typed
lambda-calculi. Instead of the usual semantic
proof style based on Tait's realizability or
Girard's “candidats de réductibilité'',
termination can be proved using a decreasing metric
over a well-founded ordering. This proof method is
applied to the simply-typed lambda-calculus and
the system of intersection types, giving the first
non-semantic proof for a polymorphic extension of
the lambda-calculus.
[ bib |
.ps.gz |
.pdf.gz |
.pdf |
.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.
|
