On Sun, May 13, 2012 at 1:07 PM, "Mark" <m...@proof-technologies.com> wrote:
> Yes, big integers is the other possibility. I'm trying to do it as light
> weight as possible, and yet keeping the user interface "conventional"
> (using
> the classic types so that integer literals supplied by the user do not have
> to be wrapped with 'Int'). However, the HOL Zero natural number syntax
> functions already use big integers, and so there is already an
> inconsistency
> in style here, and so maybe I should follow your suggestion. And yes, I
> will be switching to SML, but this is several months away, and in any case,
> I want everything to be as watertight as possible in the OCaml
> implementation.
>
Sounds good.
For your information, I am currently working on a verified compiler for
(currently a pure subset of) SML.
But it is also probably several months away from completion :)
>
> Mark.
>
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
