A Brief Overview of HOL4
TPHOLs, pp. 28-32, 2008.
holf proof assistantclassical higher order logicsimilar systemshort overviewlong lineMore(5+)
The HOLF 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 HOLF system and how it may be applied in formal verification.
Full Text (Upload PDF)
PPT (Upload PPT)