From LCF to Isabelle/HOL

Lawrence C. Paulson; Tobias Nipkow; Makarius Wenzel

doi:10.1007/s00165-019-00492-1

From LCF to Isabelle/HOL

Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel

Default

University of Cambridge

Research output: Contribution to journal › Article › peer-review

33 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 language	English
Pages (from-to)	675-698
Number of pages	24
Journal	Formal Aspects of Computing
Volume	31
Issue number	6
DOIs	https://doi.org/10.1007/s00165-019-00492-1
State	Published - 1 Dec 2019

Keywords

HOL
Interactive theorem proving
Isabelle
LCF

Access to Document

10.1007/s00165-019-00492-1

Cite this

@article{84984ee1487d4545a3b854fff506f88a,

title = "From LCF to Isabelle/HOL",

abstract = "Interactive theorem provers have developed dramatically over the past four decades, from primitive beginnings to today{\textquoteright}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.",

keywords = "HOL, Interactive theorem proving, Isabelle, LCF",

author = "Paulson, {Lawrence C.} and Tobias Nipkow and Makarius Wenzel",

note = "Publisher Copyright: {\textcopyright} 2019, The Author(s).",

year = "2019",

month = dec,

day = "1",

doi = "10.1007/s00165-019-00492-1",

language = "English",

volume = "31",

pages = "675--698",

journal = "Formal Aspects of Computing",

issn = "0934-5043",

publisher = "Association for Computing Machinery (ACM)",

number = "6",

}

TY - JOUR

T1 - From LCF to Isabelle/HOL

AU - Paulson, Lawrence C.

AU - Nipkow, Tobias

AU - Wenzel, Makarius

PY - 2019/12/1

Y1 - 2019/12/1

N2 - 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.

AB - 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.

KW - HOL

KW - Interactive theorem proving

KW - Isabelle

KW - LCF

UR - http://www.scopus.com/inward/record.url?scp=85072105912&partnerID=8YFLogxK

U2 - 10.1007/s00165-019-00492-1

DO - 10.1007/s00165-019-00492-1

M3 - Article

AN - SCOPUS:85072105912

SN - 0934-5043

VL - 31

SP - 675

EP - 698

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

IS - 6

ER -

From LCF to Isabelle/HOL

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this