Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
HOL Done Right
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.