[opentheory-users] article writer for HOL4

[Ramana Kumar]

On Tue, Sep 6, 2011 at 11:58 PM, Joe Hurd <joe at gilith.com> wrote:
> Hi Ramana,
>
>> I have (almost) written an OpenTheory article writer for HOL4. (The only thing
>> unimplemented at the moment is type definitions.)
>
> Great job! I'm looking forward to seeing its output.
>
>>  Is there a HOL4 theory anyone would particularly like packaged as an
>>  OpenTheory package?
>
> I've just had a browse through the HOL4 sources, and I think the
> "float" theory of IEEE floating point arithmetic would make a great
> addition to the current theory library.

It would be good to work up to that. For starters I'm trying to get
examples/ind_def/cl because it doesn't depend on pre-packaging
anything else above the standard library. (float and ieee would need
real and arithmetic and other stuff first.)
I'm having trouble getting even that to work at the moment - I'll
write a separate email why.

>
>>  Are there any article readers that would benefit from testing on an article
>>  generated by HOL4?
>
> Certainly the opentheory tool would benefit from any kind of testing :-)
>
>> If there are any HOL Light hackers on this list who would be interested in
>> writing an article reader for HOL Light, I'd be very interested in
>> collaborating on that.
>
> I would be very happy to write a HOL Light importer: I've been waiting
> for an excuse to do this (i.e., foreign theories to import).
>
>> I
>> think the situation at the moment is as follows (maybe this should go on the
>> OpenTheory website):
>
> I think you have it right, and I have added it to the website
>
> http://www.gilith.com/research/opentheory/
>
> By the way, do you have a home page you'd like me to link your name to?

No, thanks. My CL webpage (rk436) appears to be working but I haven't
put anything there yet.

>
> Cheers,
>
> Joe
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>