Skip to main content

TS

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,
    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

Served by Apache on Linux on seL4.