A brief overview of HOL4

Authors

Konrad Slind and Michael Norrish

University of Utah

NICTA

Abstract

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

  @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}
  }

Download

• Full text
• BibTeX