You must respect the copyrights of these authors. These scans are provided as a service to those legally entitled to make a copy of the articles under the fair use doctrine.
Georg Kreisel, On the interpretation of non-finitist proofs, Journal of Symbolic Logic 14 (1951), pp. 241–267 and Journal of Symbolic Logic 15 (1952), pp. 43–58. [pdf]
Dana S. Scott, A type-theoretical alternative to ISWIM, CUCH, OWHY, Theoretical Computer Science 121 (1993), pp. 411–440. Reprint of a privately circulated manuscript written in 1969. [pdf]
Jean H. Gallier, On Girard's “candidats de réductibilité”, Technical report MS-CIS-89-31, Department of Computer and Information Science, University of Pennsylvania (1989). [pdf]
N. G. de Bruijn, Algorithmic definition of lambda-typed lambda calculus, in: Gérard Huet and Gordon Plotkin, editors, Logical Environments, Cambridge U. P. (1993), pp. 131–146. [pdf]
Antonius J. C. Hurkens, A simplification of Girard's paradox, in: Mariangiola Dezani-Ciancaglini and Gordon Plotkin, editors, Typed Lambda Calculi and Applications, Proceedings of the Second International Conference, Springer-Verlag LNCS (1995), pp. 266–278. [pdf]
Lars Birkedal and Robert Harper, Relational interpretations of recursive types in an operational setting (summary), in: Martín Abadi and Takayasu Ito, editors, Theoretical Aspects of Computer Software, Proceedings of the 3rd International Symposium, Sendai, Japan, Springer LNCS 1281 (1997), pp. 458–490. [pdf]
Bits and pieces of Girard's doctoral thesis: Jean-Yves Girard, Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur. Université Paris VII, 1972. [pdf]