From LCF to Isabelle/HOL
Publication Date
2019-09-02Journal Title
Formal Aspects of Computing
ISSN
0934-5043
Publisher
Springer London
Volume
31
Issue
6
Pages
675-698
Language
en
Type
Article
This Version
VoR
Metadata
Show full item recordCitation
Paulson, L. C., Nipkow, T., & Wenzel, M. (2019). From LCF to Isabelle/HOL. Formal Aspects of Computing, 31 (6), 675-698. https://doi.org/10.1007/s00165-019-00492-1
Abstract
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.
Keywords
Original Article, LCF, HOL, Isabelle, Interactive theorem proving
Identifiers
s00165-019-00492-1, 492
External DOI: https://doi.org/10.1007/s00165-019-00492-1
This record's URL: https://www.repository.cam.ac.uk/handle/1810/309795
Rights
Licence:
https://creativecommons.org/licenses/by/4.0/