HaskHOL

The Main HaskHOL project page

View the Project on GitHub ecaustin/haskhol

News

01/01/2015 - Began transitioning HaskHOL’s project page to GitHub to prepare for my departure/graduation from KU.

03/01/2015 - Made a number of HaskHOL packages public (haskhol-deductive, haskhol-math, haskhol-haskell) in support of the verificatin plugin described in our ICFP’15 submission.

Description

HaskHOL is a Haskell hosted domain specific language for Higher-Order Logic (HOL) theorem proving. The goal of HaskHOL is to provide a lightweight, general purpose theorem proving library for direct use by other Haskell programs and libraries.

HaskHOL, like every other member of the HOL proof system family, follows the LCF implementation style – it starts with a sound and simple logical kernel from which more advanced features are bootstrapped. The primitive logic of HaskHOL is inspired heavily by Freek Wiedijk’s Stateless HOL and Norbert Voelker’s HOL2P; both of which are extensions of John Harrison’s HOL Light.

At the lowest level, HaskHOL’s logical kernel is a “psuedo-stateless” implementation of a HOL logic that supports limited second-order polymorphism. This logic is essentially a confluence of Wiedijk and Voelker’s logics, with a subtle modification to the stateless approach to embed hashes for comparison, rather than definitional values. This allows HaskHOL to efficiently represent and operate over its primitive data types, even in the presence of non-lazy traversals. As a brief aside, the current reliance on hashes is potentially unsound, however, that should be fixed by moving to static keys as provided by the static pointers implementation coming soon to GHC.

The stateful features of the HaskHOL system are built on top of this kernel by simulating the desired side effects via a computational monad. We find this segregation to be beneficial, as the implementation of the side effects does not need to worry about maintaining the soundness of the system, provided that the interface exposed by the kernel is respected. The haskhol-core package provides the kernel, stateful layer, and other basic functionality (parser, pretty-printer, etc.) of HaskHOL. Additional packages providing more advanced libraries are in an experimental, semi-stable state, but should be made publicly available soon.

The current focus of the HaskHOL project is developing a linkage with GHC at the compiler plugin level for the purpose of verifying Haskell code natively at compile time.

Status

The Core HaskHOL system is now publicly available on Hackage. Provided you have an up to date Haskell and Cabal installation, installing HaskHOL-Core should be as easy as running the command: cabal install haskhol-core

Additional libraries are available by request. They will be released publicly, pending a code review and documentation.

A basic tutorial is in the works, but its availability is currently unknown. In the mean time, we encourage you to consult the documentation of the previously mentioned systems, and Gordon and Melham’s Introduction to HOL, to answer any HOL questions you may have.

Papers