HOL Done Right

John Harrison.

Unpublished draft, 21st August 1995.

Abstract:

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