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" <konrad.sl...@gmail.com> 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 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 Paulson <l...@cam.ac.uk> wrote:
> 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 requires
several hours CPU time on a 2 megabyte Vax/750.”
>
> Jeff Joyce verified several versions of this computer (which he called
Tamarack) using HOL. Do any of these proofs still run? I wonder how long it
takes now?
>
> Larry
>
>
>
------------------------------------------------------------------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
