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.
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).
Kripke models and the (in)equational logic of the second-order
lambda-calculus
by Jean Gallier
transfer by anonymous ftp
.
Proving Properties of Typed lambda-Terms Using Realizability,
Covers, and Sheaves
by Jean Gallier
both
dvi
and
postscript
versions ftp-available.
Typing untyped lambda-terms, or Reducibility strikes again!
by Jean Gallier
both
dvi
and
postscript
versions ftp-available.
Parametricity and variants of Girard's $J$ operator
by Robert Harper and John Mitchell
available on the
WWW
.
or by
transfer by anonymous ftp
.