[opentheory-users] article writer for HOL4

[Joe Hurd]

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.

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

Cheers,

Joe