Trustworthy Systems

A brief overview of HOL4

Authors

Konrad Slind and Michael Norrish

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,
    address          = {Montr\'eal, Canada},
    author           = {Slind, Konrad and Norrish, Michael},
    booktitle        = {International Conference on Theorem Proving in Higher Order Logics},
    editor           = {{Otmane Ait Mohamed, C\'esar Mu\~noz and Sofi\`ene Tahar}},
    month            = aug,
    pages            = {28--32},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/1482.pdf},
    publisher        = {Springer},
    title            = {A Brief Overview of {HOL4}},
    year             = {2008}
  }

Download