HOL(ID:1150/hol001)
Higher Order Logic
- Country: uk
- Began: 1985
- Published: 1985
Higher Order Logic. A proof-generating system for higher order logic based on LCF.
HOL-88 written in ML, HOL-90 written in SML/NJ
Related languages
| Cambridge LCF |
=> |
HOL | |
Based on |
| HOL |
=> |
HOL-88 | |
Implementation |
| HOL |
=> |
HOLCF | |
Evolution of |
| HOL |
=> |
Isabelle/HOL | |
Derivation of |
References:
Gordon, M.J.C. "HOL: A Machine Oriented Formulation of Higher Order Logic", Report 68, Comp Lab U Cambridge (1985). view details
Gordon, M.J.C. et al, "Introduction to HOL", Cambridge U Press 1993 ISBN 0-521-441897
view details
Wiedijk, Freek "The Fifteen Provers of the World" view details
Abstract: We compare the styles of several proof assistants for mathematics. We present Pythagoras' proof of the irrationality of pi both informal and formalized in (1) HOL, (2) Mizar, (3) PVS, (4) Coq, (5) Otter/Ivy, (6) Isabelle/Isar, (7) Alfa/Agda, (8) ACL2, (9) PhoX, (10) IMPS, (11) Metamath, (12) Theorema, (13) Lego, (14) Nuprl, (15)Omega.
Gordon M.J.C. "From LCF to HOL: A Short History"
in
Plotkin, Stirling and Tofte (eds)
Proof, Language, and Interaction: Essays in the Honor of Robin Milner view details
Abstract: Gives the history of HOL, showing how HOL emerged from an early extension of LCF that handled a logic for describing so-called "sequential machines", with a concern towards hardware verification.
Resources - HOL-88
"
- FTP for HOL-90
"
- info for HOL-88
i
- info for HOL-90
i
|