[L4] ================================================ AMAST Links 02 01

            Papers on Higher-Order and Typed Lambda Calculi

   Abstracts of the papers listed below, together with more detailed
information (reading advice, instructions for FTP retrieval of the
full papers, etc.) are in the _full version_ of this announcement, at
URL: http://www.cs.utwente.nl/data/amast/links/v02/i01/full/HOTLCl.txt
   
   New Notions of Reduction and Non-Semantic Proofs of Beta Strong
Normalization in Typed Lambda Calculi
   by Joe Wells and A.J. Kfoury
   Boston Univ. Comp. Sci. Dept. Tech. Rep. 94-014
   _transfer by anonymous ftp_ (93K) at
URL: ftp://cs-ftp.bu.edu/techreports/94-014-strong-normalization.ps.gz

   Kripke models and the (in)equational logic of the second-order
lambda-calculus
   by Jean Gallier
   _transfer by anonymous ftp_ at
URL: ftp://ftp.cis.upenn.edu/pub/papers/gallier/kripke1.dvi.Z

   Proving Properties of Typed lambda-Terms Using Realizability,
Covers, and Sheaves
   by Jean Gallier
   both _dvi_ and _postscript_ versions ftp-available, respectively at
URL: ftp://ftp.cis.upenn.edu/pub/papers/gallier/psheaf1.dvi.Z,.ps.Z

   Typing untyped lambda-terms, or Reducibility strikes again!
   by Jean Gallier
   both _dvi_ and _postscript_ versions ftp-available, respectively at
URL: ftp://ftp.cis.upenn.edu/pub/papers/gallier/DDOreduc.dvi.Z,.ps.Z

   Parametricity and variants of Girard's $J$ operator
   by Robert Harper and John Mitchell
   available on the WWW at
URL: http://theory.stanford.edu/people/jcm/home.html
   or by _transfer by anonymous ftp_ at
URL: ftp://theory.stanford.edu/pub/jcm/girard-j.dvi