A brief overview of HOL4
Authors
University of Utah
NICTA
Abstract
The HOL4 proof assistant supports speciļ¬cation 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 HOL4 system and how it may be applied in formal verification.
BibTeX Entry
@inproceedings{Slind_Norrish_08, publisher = {Springer}, author = {Slind, Konrad and Norrish, Michael}, month = aug, editor = {{Otmane Ait Mohamed, C\'esar Mu\~noz and Sofi\`ene Tahar}}, year = {2008}, title = {A Brief Overview of {HOL4}}, booktitle = {International Conference on Theorem Proving in Higher Order Logics}, pages = {28--32}, address = {Montr\'eal, Canada} }