[1] H. P. Barendregt: The Lambda Calculus. Its syntax and semantics. (Studies in Logic and the Foundations of Mathematics 103.), North-Holland, Amsterdam 1981. MR 0622912 | Zbl 0467.03010

[2] A. Church: A formulation of the simple theory of types. J. Symb. Logic 5 (1948), 1, 56-68. MR 0001931

[3] A. Church: The Calculi of $\lambda$-conversion. (Annals of Mathematics Studies No. 6.), Princeton University Press, Princeton 1941 (1951). MR 0005274 | Zbl 0026.24205

[4] R. O. Gandy: An early proof of normalization by A. M. Turing. In: To H. B. Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism (J. R. Hindley, J. P. Seldin, eds.), Academic Press, London 1980, pp. 453 - 456. MR 0592814

[5] R. O. Gandy: Proofs of strong normalization. In: [4], pp. 457-477. MR 0592815

[6] M. H. A. Newman: On theories with a combinatorial definition of "equivalence". Ann. of Math. (2), 43 (1942), 223-243. MR 0007372 | Zbl 0060.12501

[7] D. S. Scott: Lectures on a Mathematical Theory of Computation. Oxford University Computing Laboratory, Technical Monograph PRG-19, 1981. MR 0696963

[8] D. S. Scott: Relating theories of the $\lambda$-calculus. In: [4], pp. 403 - 450. MR 0592813

[9] A. S. Troelstra (ed.): Metamathematical Investigations of Intuitionistic Arithmetic and Analysis. (Lecture Notes in Mathematics 344). Springer-Verlag, Berlin 1973. MR 0325352

[10] J. Zlatuška: HIT data model. Data bases from the functional point of view. In: Proc. 11th VLDB (A. Pirotte, Y. Vassiliou, eds.), Stockholm 1985, pp. 470-477.