Normalisation by Translation

• To: types@dcs.gla.ac.uk
• Subject: Normalisation by Translation
• From: loader <loader@maths.ox.ac.uk>
• Date: Thu, 6 Apr 1995 15:04:40 +0100
• Approved: types@dcs.gla.ac.uk

            ``Normalisation by Translation.''

A note on a nice new bright and shiny proof of strong normalisation for
system F, is now available.  The proof does not use ``reducibility
candidates'' or similar sets of terms.  Instead we use a translation on
terms to directly calculate a normalisation tree, and then use a model to
verify the correctness of this.

See either <URL:http://sable.ox.ac.uk/~loader> or anonymous FTP to
ftp.ox.ac.uk in /pub/users/loader/normal.{tex,dvi,ps}.

Ralph Loader.

• Prev: LDPL'95 Call for participation
• Next: Lectureships
• Index(es):
  • Main
  • Thread