[Prev][Next][Index][Thread]
paper available: New Proof Method for SN for Typed Lambda Calculi

To: types@dcs.gla.ac.uk

Subject: paper available: New Proof Method for SN for Typed Lambda Calculi

From: jbw@cs.bu.edu (Joe Wells)

Date: Mon, 19 Dec 1994 19:30:23 0500

Approved: types@dcs.gla.ac.uk
This note is the announcement of the availability of a paper entitled:
New Notions of Reduction and NonSemantic Proofs of Beta Strong
Normalization in Typed Lambda Calculi
by myself and A. J. Kfoury. Here is the abstract:
Two new 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 new notions of reduction. This
leads to a new way to prove beta strong normalization for typed lambda
calculi. Instead of the usual semantic proof style based on Girard's
``candidats de r\'eductibilit\'e'', termination can be proved using a
decreasing metric over a wellfounded ordering in a style more common in
the field of term rewriting. This new proof method is applied to the
simplytyped lambda calculus and the system of intersection types.
It is Boston Univ. Comp. Sci. Dept. Tech. Rep. 94014 and it is available
via anonymous FTP from the host CSFTP.BU.EDU in the directory
"techreports" as the file "94014strongnormalization.ps.gz" (93K). The
URL is:
ftp://csftp.bu.edu/techreports/94014strongnormalization.ps.gz
(Files ending with the ".gz" suffix are compressed with the "gzip"
program, which is available via anonymous FTP from the host
PREP.AI.MIT.EDU in the directory "pub/gnu" with filenames
"gzip1.2.4.msdos.exe", "gzip1.2.4.shar", "gzip1.2.4.tar", and
"gzip1.2.4.tar.gz".)

Enjoy,
Joe Wells <jbw@cs.bu.edu>
Member of the League for Programming Freedom  send email for details