[opentheory-users] article writer for HOL4

[Ramana Kumar]

On Wed, Sep 7, 2011 at 4:52 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> 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.)

Oh one thing the cl (which is combinatory logic by the way) theory
does need is inductive datatypes, which don't appear to be in the
standard library in a general form.
Since I think it's an "internal" issue, how different systems
implement datatypes, I'm temporarily putting constants like HOL4's
ind_type$recspace (out of which inductive datatypes are carved),
ind_type$CONSTR, etc., into the HOL4.Datatype namespace.
The HOL4 namespace might become more populated with such
library-implementation constants over time, or we might decide to
standardise their implementations (at least as far as the theories
supporting the libraries go)... thoughts?

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