From LCF to Isabelle/HOL

Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel

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.




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}