[LK] ================================================ AMAST Links 02 04

                     Normalisation by Translation
                             Ralph Loader

  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.

  The _note_ can be obtained from URL: http://sable.ox.ac.uk/~loader 
or by FTP from _directory_ URL: ftp://ftp.ox.ac.uk/pub/users/loader/ 
where the LaTeX, DVI and PostScript versions are available; the files
are GNU-compressed, and are resp. called normal.{tex,dvi,ps}.gz