Technical reports
HOL
A proof generating system for higher-order logic
January 1987, 56 pages
DOI: 10.48456/tr-103
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 behavioural 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.
Full text
PDF (3.2 MB)
BibTeX record
@TechReport{UCAM-CL-TR-103, author = {Gordon, Mike}, title = {{HOL : A proof generating system for higher-order logic}}, year = 1987, month = jan, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-103.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-103}, number = {UCAM-CL-TR-103} }