Re: [Hol-info] "Gordon Computer"

2018-04-07 Thread Thomas Tuerk
e: >> >> 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 ap

Re: [Hol-info] "Gordon Computer"

2018-04-07 Thread Michael.Norrish
.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 a

Re: [Hol-info] "Gordon Computer"

2018-04-06 Thread Lawrence Paulson
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

Re: [Hol-info] "Gordon Computer"

2018-04-05 Thread Ramana Kumar
It doesn't look too bad to me - happy to port them if you like. On 5 April 2018 at 12:36, Lawrence Paulson wrote: > I have just managed to locate Jeff Joyce's "Tamarack-2" files, which he > describes as slightly simplified compared with the original Gordon > computer. They are

[Hol-info] "Gordon Computer"

2018-04-05 Thread Lawrence Paulson
I have just managed to locate Jeff Joyce's "Tamarack-2" files, which he describes as slightly simplified compared with the original Gordon computer. They are dated 1989 and the comments suggest that they are for HOL88. I guess they will bring back the memories for some people. But it would