Normalisation by Translation

            ``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.