Hi Gergely:

  That work was done in the late 1980s. It may be that
Brian Graham still has the proof scripts available. However,
it would probably be very difficult to build a version of HOL
that would run the scripts as-is. An interesting project would
be to re-do the theories using up-to-date technology.

Cheers,
Konrad.



On Sun, Jun 1, 2014 at 10:47 AM, Gergely Buday <gbu...@gmail.com> wrote:

> Dear HOL users,
>
> I have found the book by Brian T. Graham about a formalisation of an
> SECD microprocessor using the HOL proof assistant.
>
> I have not found the proof script. Do you know whether it is
> proprietary or available for research purposes?
>
> - Gergely
>
>
> ------------------------------------------------------------------------------
> Time is money. Stop wasting it! Get your web API in 5 minutes.
> www.restlet.com/download
> http://p.sf.net/sfu/restlet
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and their 
applications. Written by three acclaimed leaders in the field, 
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/NeoTech
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Reply via email to