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> 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
