Trustworthy Systems

A brief overview of HOL4


Konrad Slind and Michael Norrish

University of Utah



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

    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         = {},
    publisher        = {Springer},
    title            = {A Brief Overview of {HOL4}},
    year             = {2008}