Skip to main content


A brief overview of HOL4


Konrad Slind and Michael Norrish

University of Utah



The HOL4 proof assistant supports specification 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

    publisher        = {Springer},
    author           = {Slind, Konrad and Norrish, Michael},
    month            = aug,
    editor           = {{Otmane Ait Mohamed, César Muñoz and Sofiène Tahar}},
    year             = {2008},
    title            = {A Brief Overview of {HOL4}},
    booktitle        = {International Conference on Theorem Proving in Higher Order Logics},
    pages            = {28-32},
    address          = {Montréal, Canada}


Served by Apache on Linux on seL4.