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
]