<div dir="ltr">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.<br><div class="gmail_extra"><br><div class="gmail_quote">On 29 December 2015 at 17:53, Ramana Kumar <span dir="ltr"><<a href="mailto:ramana@member.fsf.org" target="_blank">ramana@member.fsf.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><span>On 29 December 2015 at 08:41, Yannick <span dir="ltr"><<a href="mailto:yannick_duchene@yahoo.fr" target="_blank">yannick_duchene@yahoo.fr</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><u></u>
<div><div>Hi people out there, I'm new here.</div><div><br></div><div>May be my mind is buggy, I was sure to recall there was an OpenTheory reader/writer for Coq. Now looking at <a href="http://www.gilith.com/research/opentheory/" target="_blank">http://www.gilith.com/research/opentheory/</a> , I can't see it.</div></div></blockquote><div><br></div></span><div>You might be thinking of Holide. There is a link at <a href="http://dedukti.gforge.inria.fr/" target="_blank">http://dedukti.gforge.inria.fr/</a>, but it seems to be 404 at the moment. Ask the authors?<br><br></div><div>Another possibility is <a href="https://www.lri.fr/~keller/Recherche/hollightcoq.html" target="_blank">https://www.lri.fr/~keller/Recherche/hollightcoq.html</a>, but I think it's only one-way (and not the direction you need).<br></div><span><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div><br></div><div>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.</div></div></blockquote><div><br></div></span><div>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.<br></div><span><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div><br></div><div>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.</div></div></blockquote><div><br></div></span><div>Writing proofs in HOL4 or HOL Light is not as frightening as you might think :)<br></div><span><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div><br></div><div>That's about the picture. If possible, I would prefer to use Coq, just only if it can writes OpenTheory files.</div></div></blockquote><div><br></div></span><div>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.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span><div><div><br></div><div>I welcome any comments and suggestions.</div><div><br></div><div>Have a nice day as much as possible, and happy new year 2016.</div><div><br></div><div><br></div><div><div>-- </div><div>Yannick Duchêne</div></div></div><br></span>_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
<br></blockquote></div><br></div></div>
</blockquote></div><br></div></div>