HOL: A Proof Generating System for Higher-Order Logic
The work
| Authors | Mike Gordon |
|---|---|
| Editors | |
| Type | techreport |
| Year | 1987 |
| Citekey | gordon1987hol |
Where it appeared
| Publisher | University of Cambridge Computer Laboratory |
|---|---|
| Number in series | UCAM-CL-TR-103 |
| School | University of Cambridge Computer Laboratory |
Identifiers
| DOI | 10.48456/tr-103 |
|---|---|
| report_number | UCAM-CL-TR-103 |
| ISSN | 1476-2986 |
Access
| Landing page | https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-103.html |
|---|
Related
| Distinct from | camilleri1986hardware |
|---|---|
| Distinct from | camilleri1988simulation |
| Distinct from | cohn1986mechanized |
| Distinct from | cohn1987proof |
| Distinct from | cohn1988correctness |
| Distinct from | dhingra1987formal |
| Distinct from | gordon1983lcflsm |
| Distinct from | gordon1985hol |
| Distinct from | gordon1985why |
| Distinct from | herbert1988case |
| Distinct from | joyce1988formal |
| Distinct from | leeser1988reasoning |
| Distinct from | melham1990formalizing |
| Distinct from | melham1993higher |
From bibtex.
Abstract
HOL is a version of Robin Milner's LCF theorem proving system for higher-order logic. It is currently being used to investigate how various levels of hardware behaviour can be rigorously modelled and how the resulting behavioral representations can be the basis for verification by mechanized formal proof. This paper starts with a tutorial introduction to the meta-language ML. The version of higher-order logic implemented in the HOL system is then described. This is followed by an introduction to goal-directed proof with tactics and tacticals. Finally, there is a little example showing the system in action. This example illustrates how HOL can be used for hardware verification.
A copy is held
pdf, 3.0 MB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-15 22:37 UTC |
| Approved by | a person 2026-09-23 14:10 UTC |
Filed under
Cite it as
@techreport{gordon1987hol,
title = {HOL: A Proof Generating System for Higher-Order Logic},
author = {Mike Gordon},
year = {1987},
publisher = {University of Cambridge Computer Laboratory},
school = {University of Cambridge Computer Laboratory},
issn = {1476-2986},
doi = {10.48456/tr-103},
}
This record lives at https://refs.drheap.org/gordon1987hol/ and will keep doing so.