106 BIBLIOGRAPHY
Gordon, M. J. C., Milner, R., and Wadsworth, C. P. (1979) Edinburgh LCF: A
Mechanised Logic of Computation, Volume 78 of Lecture Notes in Computer Sci-
ence. Springer-Verlag.
Harrison, J. (1995) Inductive definitions: automation and application. In Windley,
P. J., Schubert, T., and Alves-Foss, J. (eds.), Higher Order Logic Theorem Proving
and Its Applications: Proceedings of the 8th International Workshop, Volume 971
of Lecture Notes in Computer Science, Aspen Grove, Utah, pp. 200–213. Springer-
Verlag.
Harrison, J. (1996) Optimizing proof search in model elimination. In McRobbie,
M. A. and Slaney, J. K. (eds.), 13th International Conference on Automated
Deduction, Volume 1104 of Lecture Notes in Computer Science, New Brunswick,
NJ, pp. 313–327. Springer-Verlag.
Heijenoort, J. v. (ed.) (1967) From Frege to G¨odel: A Source Book in Mathematical
Logic 1879–1931. Harvard University Press.
Henkin, L. (1963) A theory of propositional types. Fundamenta Mathematicae, 52,
323–344.
Jones, R. and Lins, R. (1996) Garbage collection: algorithms for automatic dynamic
memory management. Wiley.
Knaster, B. (1927) Un th´eor`eme sur les fonctions d’ensembles. Annales de la Soci´et´e
Polonaise de Math´ematique, 6, 133–134. Volume published in 1928.
Knuth, D. E. (1969) The Art of Computer Programming; Volume 2: Seminumer-
ical Algorithms. Addison-Wesley Series in Computer Science and Information
processing. Addison-Wesley.
Lagarias, J. (1985) The 3x + 1 problem and its generalizations. The
American Mathematical Monthly, 92, 3–23. Available on the Web as
http://www.cecm.sfu.ca/organics/papers/lagarias/index.html.
Lambek, J. and Scott, P. J. (1986) Introduction to higher order categorical logic,
Volume 7 of Cambridge studies in advanced mathematics. Cambridge University
Press.
Loveland, D. W. (1968) Mechanical theorem-proving by model elimination. Journal
of the ACM , 15, 236–251.
Mairson, H. G. (1990) Deciding ML typability is complete for deterministic expo-
nential time. In Conference Record of the Seventeenth Annual ACM Symposium
on Principles of Programming Languages (POPL), San Francisco, pp. 382–401.
Association for Computing Machinery.
Martin, U. and Nipkow, T. (1990) Ordered rewriting and confluence. In Stickel,
M. E. (ed.), 10th International Conference on Automated Deduction, Volume
449 of Lecture Notes in Computer Science, Kaiserslautern, Federal Republic of
Germany, pp. 366–380. Springer-Verlag.
Mauny, M. (1995) Functional programming using CAML Light. Available on the
Web from http://pauillac.inria.fr/caml/tutorial/index.html.
Miller, D. (1991) A logic programming language with lambda-abstraction, function
variables and simple unification. Journal of Logic and Computation, 1, 497–536.