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.