1

McCarthy, J. A Basis for a mathematical theory of computation. In Computer Programming and Formal Systems, Braffort and D. Hirshberg, Eds., North-Holland Pub. Co., Amsterdam, 1963.

2

Kleene, S.C. Introduction to Metamathematies, Nostrand, New York, 1950.

3

John McCarthy, LISP 1.5 Programmer's Manual, The MIT Press, 1962

4

Landin, P.J. The mechanical evaluation of expression. Computer J. 6, 4 (Jan. 1964).

5

Evans, A. PAL---A reference manual and primer. Dep. of Elec. Eng.,MIT Cambridge, Mass., 1969. (unpublished notes)

6

Reynolds, J.C. Gendanken: A simple typeless language. Rep. 7621 Argonne Nat. Lab., 1969.

7

Morris, J.H. X-calculus models of programming languages. D. Th., Sloan School of Management, MIT MAC Rep. TR-57, Mm, Cambridge, Mass.

8

Zohar Manna , Amir Pnueli, Formalization of properties of recursively defined functions, Proceedings of the first annual ACM symposium on Theory of computing, p.201-210, May 05-07, 1969, Marina del Rey, California, United States  [doi>10.1145/800169.805434]

9

Elliott Mendelson, Introduction to mathematical logic (3rd ed.), Wadsworth Publ. Co., Belmont, CA, 1987

10

Paterson, M.S. Program Schemata. In Machine Intelligence 3, Michie, Ed., American Elsevier, New York, 1963, pp. 19-32.

11

Manna, Z. and McCarthy, J. Properties of programs and partial function logic. In Machine Intelligence 5, B. Meltzer and Michie, Eds., American Elsevier, New York, 1970.

12

Scott, D. A type theoretical alternative to ISWIM, CUCH, OWHY. Unpublished notes, Oxford U., 1969.

13

Scott, D. A mathematical theory of computation. Unpublished notes, 1970.

14

Park, D. Fixpoint induction and proofs of program properties. In Machine Intelligence 5, B. Meltzer and D. Michie, Eds., American Elsevier, New York, 1970.

15

Floyd, R.W. Assigning meanings to programs. Applied Mathematics Symposia 19, AMS, Providence, R.I., 1967.

Zohar Manna , Jean Vuillemin, Fixpoint approach to the theory of computation, Communications of the ACM, v.15 n.7, p.528-536, July 1972

R. D. Tennent, The denotational semantics of programming languages, Communications of the ACM, v.19 n.8, p.437-453, Aug. 1976

R. S. Bird, Notes on recursion elimination, Communications of the ACM, v.20 n.6, p.434-439, June 1977

Zohar Manna , Stephen Ness , Jean Vuillemin, Inductive methods for proving properties of programs, ACM SIGACT News

F. L. Bauer, Programming as an evolutionary process, Proceedings of the 2nd international conference on Software engineering, p.223-234, October 13-15, 1976, San Francisco, California, United States

R. S. Bird, Improving programs by the introduction of recursion, Communications of the ACM, v.20 n.11, p.856-863, Nov. 1977

Zohar Manna , Stephen Ness , Jean Vuillemin, Inductive methods for proving properties of programs, Communications of the ACM, v.16 n.8, p.491-502, Aug. 1973

John H. Williams, On the Development of the Algebra of Functional Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.4, p.733-757, Oct. 1982

Ali Mili , Jules Desharnais, A system for classifying program verification methods: Assigning meanings to program verification methods, Proceedings of the 7th international conference on Software engineering, p.499-509, March 26-29, 1984, Orlando, Florida, United States

Zohar Manna, Computation of recursive programs: theory vs practice, Proceedings of the November 16-18, 1971, fall joint computer conference, November 16-18, 1971, Las Vegas, Nevada

T. A. Linden, A summary of progress toward proving program correctness, Proceedings of the December 5-7, 1972, fall joint computer conference, part I, December 05-07, 1972, Anaheim, California

James H. Morris, Jr.: colleagues