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.


From: Lawrence Paulson <>
Date: Friday, 6 April 2018 at 21:27
To: Ramana Kumar <>, HOL-info list 
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 


On 5 Apr 2018, at 14:31, Ramana Kumar 
<<>> wrote:

Attached is a port of<>, 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 
<<>> 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.


On 5 Apr 2018, at 13:41, Ramana Kumar 
<<>> wrote:

It doesn't look too bad to me - happy to port them if you like.


Check out the vibrant tech community on one of the world's most
engaging tech sites,!
hol-info mailing list

Reply via email to