A brief overview of HOL4

Konrad Slind; Michael Norrish

doi:10.1007/978-3-540-71067-7_6

A brief overview of HOL4

Konrad Slind^*, Michael Norrish

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

219 Citations (Scopus)

Abstract

The HOLF proof assistant supports specification and proof in classical higher order logic. It is the latest in a long line of similar systems. In this short overview, we give an outline of the HOLF system and how it may be applied in formal verification.

Original language	English
Title of host publication	Theorem Proving in Higher Order Logics - 21st International Conference, TPHOLs 2008, Proceedings
Publisher	Springer Verlag
Pages	28-32
Number of pages	5
ISBN (Print)	3540710655, 9783540710653
DOIs	https://doi.org/10.1007/978-3-540-71067-7_6
Publication status	Published - 2008
Externally published	Yes
Event	21st International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2008 - Montreal, QC, Canada Duration: 18 Aug 2008 → 21 Aug 2008

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	5170 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	21st International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2008
Country/Territory	Canada
City	Montreal, QC
Period	18/08/08 → 21/08/08

Access to Document

10.1007/978-3-540-71067-7_6

Cite this

Slind, K., & Norrish, M. (2008). A brief overview of HOL4. In Theorem Proving in Higher Order Logics - 21st International Conference, TPHOLs 2008, Proceedings (pp. 28-32). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5170 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-540-71067-7_6

@inproceedings{2413d9df85a8491f855ef5f207faa9c6,

title = "A brief overview of HOL4",

abstract = "The HOLF proof assistant supports specification and proof in classical higher order logic. It is the latest in a long line of similar systems. In this short overview, we give an outline of the HOLF system and how it may be applied in formal verification.",

author = "Konrad Slind and Michael Norrish",

year = "2008",

doi = "10.1007/978-3-540-71067-7_6",

language = "English",

isbn = "3540710655",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "28--32",

booktitle = "Theorem Proving in Higher Order Logics - 21st International Conference, TPHOLs 2008, Proceedings",

address = "Germany",

note = "21st International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2008 ; Conference date: 18-08-2008 Through 21-08-2008",

}

Slind, K & Norrish, M 2008, A brief overview of HOL4. in Theorem Proving in Higher Order Logics - 21st International Conference, TPHOLs 2008, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5170 LNCS, Springer Verlag, pp. 28-32, 21st International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2008, Montreal, QC, Canada, 18/08/08. https://doi.org/10.1007/978-3-540-71067-7_6

A brief overview of HOL4. / Slind, Konrad; Norrish, Michael.
Theorem Proving in Higher Order Logics - 21st International Conference, TPHOLs 2008, Proceedings. Springer Verlag, 2008. p. 28-32 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5170 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - A brief overview of HOL4

AU - Slind, Konrad

AU - Norrish, Michael

PY - 2008

Y1 - 2008

N2 - The HOLF proof assistant supports specification and proof in classical higher order logic. It is the latest in a long line of similar systems. In this short overview, we give an outline of the HOLF system and how it may be applied in formal verification.

AB - The HOLF proof assistant supports specification and proof in classical higher order logic. It is the latest in a long line of similar systems. In this short overview, we give an outline of the HOLF system and how it may be applied in formal verification.

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

U2 - 10.1007/978-3-540-71067-7_6

DO - 10.1007/978-3-540-71067-7_6

M3 - Conference contribution

SN - 3540710655

SN - 9783540710653

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 28

EP - 32

BT - Theorem Proving in Higher Order Logics - 21st International Conference, TPHOLs 2008, Proceedings

PB - Springer Verlag

T2 - 21st International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2008

Y2 - 18 August 2008 through 21 August 2008

ER -

A brief overview of HOL4

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this