From LCF to Isabelle/HOL
Interactive theorem provers have developed dramatically over the past
four decades, from primitive beginnings to today's powerful
systems. Here, we focus on Isabelle/HOL and its distinctive
strengths. They include automatic proof search, borrowing techniques
from the world of first order theorem proving, but also the automatic
search for counterexamples. They include a highly readable structured
language of proofs and a unique interactive development environment
for editing live proof documents. Everything rests on the foundation
conceived by Robin Milner for Edinburgh LCF: a proof kernel, using
abstract types to ensure soundness and eliminate the need to store
proofs. Compared with the research prototypes of the 1970s, Isabelle
is a practical and versatile tool. It is used by system designers,
mathematicians and many others.
pdf
Springer's web page
BibTeX:
@article{PaulsonNW-FAC19,
author={Lawrence C. Paulson and Tobias Nipkow and Makarius Wenzel},
title={From LCF to Isabelle/HOL},
journal={Formal Aspects of Computing},volume=31,pages={675--698},year=2019}