From LCF to Isabelle/HOL

Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel

Research output: Contribution to journalArticlepeer-review

29 Scopus citations

Abstract

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.

Original languageEnglish
Pages (from-to)675-698
Number of pages24
JournalFormal Aspects of Computing
Volume31
Issue number6
DOIs
StatePublished - 1 Dec 2019

Keywords

  • HOL
  • Interactive theorem proving
  • Isabelle
  • LCF

Fingerprint

Dive into the research topics of 'From LCF to Isabelle/HOL'. Together they form a unique fingerprint.

Cite this