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 or by FTP from directory where the LaTeX, DVI and PostScript versions are available; the files are GNU-compressed, and are resp. called normal.{tex,dvi,ps}.gz