HOL Done Right

John Harrison.

Unpublished draft, 21st August 1995.


In our opinion, history and compatibility considerations have rendered existing HOL implementations rather messy and badly organized. We describe how, building on joint work with Konrad Slind, we have produced a re-engineered HOL. Various experiments have been tried on this `toy' version, and we will report the results.

DVI or PostScript or PDF