References

BM79

Robert Boyer and J. Strother Moore. A Computational Logic. Academic Press, 1979.

Car77

Robert S. Cartwright. A practical formal semantic definition and verification system for typed lisp. Phd dissertation, stanford university, 1977.

CDE 98

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Marti-Oliet, and J. Meseguer. Metalevel Computation in Maude. In C. Kirchner and H. Kirchner, editors, 2nd International Workshop on Rewriting Logic and its Applications, WRLA'98, volume 15 of Electronic Notes in Theoretical Computer Science, 1998. URL: http://www.elsevier.nl/locate/entcs/volume15.html.

CM79

Robert Cartwright and John McCarthy. Recursive programs as functions in a first order theory. In Proceedings of the International Conference on Mathematical Studies of Information Processing, Kyoto, Japan, 1979.

Gro99

The Maude Group. The Maude system, 1999. See http://maude.csl.sri.com/.

HMST95

F. Honsell, I. A. Mason, S. F. Smith, and C. L. Talcott. A Variable Typed Logic of Effects. Information and Computation, 119(1):55-90, 1995.

Kle52

Stephen C. Kleene. Introduction to Metamathematics. Van Nostrand, 1952.

Mas86

I. A. Mason. The Semantics of Destructive Lisp. PhD thesis, Stanford University, 1986. Also available as CSLI Lecture Notes No. 5, Center for the Study of Language and Information, Stanford University.

McC60

J. McCarthy. Recursive functions of symbolic expressions and their computation by machine, part 1. Comm. A.C.M., 3:184-195, 1960.

McC62

John McCarthy. Checking mathematical proofs by computer. In Proceedings Symposium on Recursive Function Theory (1961). American Mathematical Society, 1962.

McC63

John McCarthy. A Basis for a Mathematical Theory of Computation. In P. Braffort and D. Hirschberg, editors, Computer Programming and Formal Systems, pages 33-70. North-Holland, Amsterdam, 1963.

McC80

John McCarthy. Circumscription--A Form of Non-Monotonic Reasoning. Artificial Intelligence, 13:27-39, 1980. Reprinted in [McC90].

McC81

John McCarthy. History of lisp. In Richard L. Wexelblat, editor, History of programming languages. Academic Press, 1981. Reprinted from Proceedings of the ACM Conference on the History of Programming Languages, Los Angeles, 1977.

McC90

John McCarthy. Formalizing Common Sense: Papers by John McCarthy. Ablex Publishing Corporation, 355 Chestnut Street, Norwood, NJ 07648, 1990.

McC96

John McCarthy. elephant 2000. Technical report, Stanford Formal Reasoning Group, 1996. Available only as http://www-formal.stanford.edu/jmc/elephant.html.

ML 66

John McCarthy, Michael Levin, et al. LISP 1.5 Programmer's Manual. MIT, 1966.

Wil97

Wilson97. Cars and their enemies. Commentary, pages 17-23, July 1997.

WM78

Daniel Weinreb and David Moon. Lisp machine manual. Technical report, M.I.T. Artificial Intelligence Laboratory, 1978.