Show simple item record

dc.contributor.authorPaulson, Lawrence C.
dc.contributor.authorNipkow, Tobias
dc.contributor.authorWenzel, Makarius
dc.date.accessioned2020-09-01T15:15:19Z
dc.date.available2020-09-01T15:15:19Z
dc.date.issued2019-09-02
dc.date.submitted2019-03-25
dc.identifier.issn0934-5043
dc.identifier.others00165-019-00492-1
dc.identifier.other492
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/309795
dc.description.abstractAbstract: 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.
dc.languageen
dc.publisherSpringer London
dc.subjectOriginal Article
dc.subjectLCF
dc.subjectHOL
dc.subjectIsabelle
dc.subjectInteractive theorem proving
dc.titleFrom LCF to Isabelle/HOL
dc.typeArticle
dc.date.updated2020-09-01T15:15:18Z
prism.endingPage698
prism.issueIdentifier6
prism.publicationNameFormal Aspects of Computing
prism.startingPage675
prism.volume31
dc.identifier.doi10.17863/CAM.56894
dcterms.dateAccepted2019-08-09
rioxxterms.versionofrecord10.1007/s00165-019-00492-1
rioxxterms.versionVoR
rioxxterms.licenseref.urihttps://creativecommons.org/licenses/by/4.0/
dc.contributor.orcidPaulson, Lawrence C. [0000-0003-0288-4279]
dc.identifier.eissn1433-299X


Files in this item

Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record