[Prev][Next][Index][Thread]

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


This note is the announcement of the availability of a paper entitled:

  New Notions of Reduction and Non-Semantic 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 well-founded ordering in a style more common in
  the field of term rewriting.  This new proof method is applied to the
  simply-typed lambda calculus and the system of intersection types.

It is Boston Univ. Comp. Sci. Dept. Tech. Rep. 94-014 and it is available
via anonymous FTP from the host CS-FTP.BU.EDU in the directory
"techreports" as the file "94-014-strong-normalization.ps.gz" (93K).  The
URL is:

  ftp://cs-ftp.bu.edu/techreports/94-014-strong-normalization.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
"gzip-1.2.4.msdos.exe", "gzip-1.2.4.shar", "gzip-1.2.4.tar", and
"gzip-1.2.4.tar.gz".)

-- 
Enjoy,

Joe Wells <jbw@cs.bu.edu>
Member of the League for Programming Freedom --- send e-mail for details