Thanks for your kind answer, but I'm really looking for the opposite: to run
the classic old examples using the latest technology. It's a way of measuring
the progress of our field.
Larry
> On 4 Apr 2018, at 21:59, Chun Tian wrote:
>
> Hi,
>
> I didn't follow the entire discussions about “Go
Hi,
I didn't follow the entire discussions about “Gordon computer”, but if you just
want to run HOL88, that’s easy.
All you need to do is an Ubuntu 16.04 Linux environment (or Debian GNU/Linux),
and install the “hol88” (and other hol88-*) packages [1, 2]. Latest version is
“2.02.19940316”.
Bu
On 2 Apr 2018, at 10:47,
wrote:
>
> I take it there's nothing in the CL area that used to be something like
> /usr/groups/hvg ?
I couldn't find it, though it may simply have moved somewhere. More worrying is
that none of the older links on this page work anymore:
http://www.cl.cam.ac.uk/res
I take it there's nothing in the CL area that used to be something like
/usr/groups/hvg ?
Michael
On 2/4/18, 08:41, "Konrad Slind" wrote:
The proofs might still run. I'd be keen to help get them going, if
they can be dug up. After Tamarack, Brian Graham verified a
hardware-level S
The proofs might still run. I'd be keen to help get them going, if
they can be dug up. After Tamarack, Brian Graham verified a
hardware-level SECD machine while a student of Graham Birtwistle.
Perhaps they have running versions of those proofs.
Konrad
On Sun, Apr 1, 2018 at 4:39 AM, Lawrence Paul
In 1983, using LCF_LSM, Mike verified his computer with the comment “The entire
specification and verification described here took several months, but this
includes some extending and debugging of LCF_LSM … it would take me two to four
weeks to do another similar exercise now. The complete proof r
