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