Bibliography
Aczel, P. (1991) An introduction to inductive definitions. In Barwise, J. and Keisler,
H. (eds.), Handbook of mathematical logic, Volume 90 of Studies in Logic and the
Foundations of Mathematics, pp. 739–782. North-Holland.
Backus, J. (1978) Can programming be liberated from the von Neumann style? A
functional style and its algebra of programs. Communications of the ACM , 21,
613–641.
Beeson, M. J. (1984) Foundations of constructive mathematics: metamathematical
studies, Volume 3 of Ergebnisse der Mathematik und ihrer Grenzgebiete. Springer-
Verlag.
Camilleri, J. and Melham, T. (1992) Reasoning with inductively defined relations
in the HOL theorem prover. Technical Report 265, University of Cambridge
Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2
3QG, UK.
Carnap, R. (1937) The Logical Syntax of Language. International library of psychol-
ogy, philosophy and scientific method. Routledge & Kegan Paul. Translated from
‘Logische Syntax der Sprache’ by Amethe Smeaton (Countess von Zeppelin), with
some new sections not in the German original.
Church, A. (1940) A formulation of the Simple Theory of Types. Journal of Symbolic
Logic, 5, 56–68.
Curry, H. B. (1930) Grundlagen der Kombinatorischen Logik. American Journal of
Mathematics, 52, 509–536, 789–834.
Davis, M. D., Sigal, R., and Weyuker, E. J. (1994) Computability, complexity, and
languages: fundamentals of theoretical computer science (2nd ed.). Academic
Press.
Frege, G. (1893) Grundgesetze der Arithmetik begriffsschrift abgeleitet. Jena. Par-
tial English translation by Montgomery Furth in ‘The basic laws of arithmetic.
Exposition of the system’, University of California Press, 1964.
Gordon, M. J. C. (1982) Representing a logic in the LCF metalanguage. In N´eel,
D. (ed.), Tools and notions for program construction: an advanced course, pp.
163–185. Cambridge University Press.
Gordon, M. J. C. (2000) From LCF to HOL: A short history. In Plotkin, G., Stirling,
C., and Tofte, M. (eds.), Proof, language, and interaction: essays in honour of
Robin Milner. MIT Press.
Gordon, M. J. C. and Melham, T. F. (1993) Introduction to HOL: a theorem proving
environment for higher order logic. Cambridge University Press.
105