[opentheory-users] Is OpenTheory usable with Coq?

[Ramana Kumar]

I should add that for HOL4 (and HOL Light, I think) there are editor-based
interfaces (for Vim and for Emacs, at least) so you are not confined to
using only the read-eval-print loop.

On 29 December 2015 at 17:53, Ramana Kumar <ramana at member.fsf.org> wrote:

> On 29 December 2015 at 08:41, Yannick <yannick_duchene at yahoo.fr> wrote:
>
>> Hi people out there, I'm new here.
>>
>> May be my mind is buggy, I was sure to recall there was an OpenTheory
>> reader/writer for Coq. Now looking at
>> http://www.gilith.com/research/opentheory/ , I can't see it.
>>
>
> You might be thinking of Holide. There is a link at
> http://dedukti.gforge.inria.fr/, but it seems to be 404 at the moment.
> Ask the authors?
>
> Another possibility is
> https://www.lri.fr/~keller/Recherche/hollightcoq.html, but I think it's
> only one-way (and not the direction you need).
>
>
>>
>> I know there is a reader for Isabell/HOL. Unfortunately, I'm rather
>> looking for a proof environment with a writer, as I bother about saving
>> proofs.
>>
>
> I am interested in producing a writer for Isabelle/HOL eventually (some
> time over the next year hopefully). It could be good to combine efforts.
>
>
>>
>> If this is useful, I may draw the picture. I'm learning to effectively
>> use ATS, a language with dependent types, linear types, inductive
>> definitions and proofs. It's a very nice language, however and for good
>> reasons, not suited to prove properties of as an example, inductive
>> definitions (it mainly target programming issues, that is, ensuring
>> pre/post conditions, resources tracking and the likes). I'm planning to
>> export inductive definition using the abstract syntax tree output ATS
>> provides, then prove properties of these inductive definitions, outside of
>> ATS and save these proofs in a standard format (luckily, OpenTheory
>> exists). I had some short past experience with Isabelle/HOL and Coq. I like
>> Isabelle/HOL for being HOL, but don't really like the language and even
>> less like the editor. So I tough about Coq and CoqIDE, which seems more
>> usable to me, as much the language and the IDE, although I don't really
>> know its logic, seemingly a superset of HOL. Unfortunately, it does not
>> seems to support OpenTheory. So may be HOL Light, but I never used it, and
>> am afraid of writing proofs in a TTy like interface.
>>
>
> Writing proofs in HOL4 or HOL Light is not as frightening as you might
> think :)
>
>
>>
>> That's about the picture. If possible, I would prefer to use Coq, just
>> only if it can writes OpenTheory files.
>>
>
> If you work in a restricted subset of Coq, it may be possible to create a
> translation from Coq's proof terms to OpenTheory format. It might be worth
> looking into that, if you're interested. Let me know.
>
>
>>
>> I welcome any comments and suggestions.
>>
>> Have a nice day as much as possible, and happy new year 2016.
>>
>>
>> --
>> Yannick Duchêne
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20151229/3e453146/attachment.html>