From LCF to HOL: a short history

MICHAEL J. C. GORDON
University of Cambridge
Computer Laboratory
Room FE19
William Gates Building
JJ Thomson Avenue
Cambridge CB3 0FD
United Kingdom
work phone: +44 1223 334627
work fax: +44 1223 334678
email: mjcg@cl.cam.ac.uk

Abstract
The original LCF system was a proof-checking program developed at Stanford University by Robin Milner in 1972. Descendents of LCF now form a thriving paradigm in computer assisted reasoning. Many of the developments of the last 25 years have been due to Robin Milner, whose influence on the field of automated reasoning has been diverse and profound. One of the descendents of LCF is HOL, a proof assistant for higher order logic originally developed for reasoning about hardware. The multi-faceted contribution of Robin Milner to the development of HOL is remarkable. Not only did he invent the LCF-approach to theorem proving, but he also designed the ML programming language underlying it and the innovative polymorphic type system used both by ML and the LCF and HOL logics. Code Milner wrote is still in use today, and the design of the hardware verification system LCF_LSM (a now obsolete stepping stone from LCF to HOL) was inspired by Milner's Calculus of Communicating Systems (CCS).
[postscript | pdf ]


The paper appeared in Proof, Language, and Interaction, by G. Plotkin (Editor), Colin P. Stirling (Editor), Mads Tofte (Editor). MIT Press, 2000; ISBN: 0262161885.