Thanks for digging out this material Larry! I’d be very happy to see it added
to our examples directory.
Ramana, let me know if you want to make the initial commits. I suggest we can
have an examples/hardware with an appropriate README.
Best,
Michael
From: Lawrence Paulson <l...@cam.ac.uk>
Date: Friday, 6 April 2018 at 21:27
To: Ramana Kumar <ramana.ku...@cl.cam.ac.uk>, HOL-info list
<hol-info@lists.sourceforge.net>
Subject: Re: [Hol-info] "Gordon Computer"
I am not sure who is in charge of HOL4 these days. Would it be possible to add
this as an example to HOL4? If people are interested, I found many other
examples. Here are just two of them:
* the specification and verification of some CMOS adders
* Transistor Implementation of a n-bit Counter
I also found Mike's original computer, which is a slightly larger example than
Tamarack.
Larry
On 5 Apr 2018, at 14:31, Ramana Kumar
<ramana.ku...@cl.cam.ac.uk<mailto:ramana.ku...@cl.cam.ac.uk>> wrote:
Attached is a port of tamarack.ml<http://tamarack.ml/>, which seems to just be
definitions. I guess the proofs might be harder to port, but I haven't looked...
They could be added to HOL/examples in the HOL4 distribution -- if I find time
to port them later (must leave it for now though..)
On 5 April 2018 at 14:02, Lawrence Paulson
<l...@cam.ac.uk<mailto:l...@cam.ac.uk>> wrote:
It would be nice to give them a permanent home, perhaps as part of the HOL4
distribution. Also I may create a small memorial page for Mike and could
include it there.
I found mountains of old stuff in Mike's file space, though sadly, much of it
is protected.
Larry
On 5 Apr 2018, at 13:41, Ramana Kumar
<ramana.ku...@cl.cam.ac.uk<mailto:ramana.ku...@cl.cam.ac.uk>> wrote:
It doesn't look too bad to me - happy to port them if you like.
<tamarackScript.sml>
------------------------------------------------------------------------------
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
