<!DOCTYPE html><html><head>
<style type="text/css">body { font-family:'DejaVu Sans Mono'; font-size:12px}</style>
<style type="text/css">body { font-family:'DejaVu Sans Mono'; font-size:12px}</style>
</head>
<body><br><br>------- Forwarded message -------<br>From: Yannick <yannick_duchene@yahoo.fr><br>To: "Ramana Kumar" <ramana@member.fsf.org><br>Cc:<br>Subject: Re: [opentheory-users] Is OpenTheory usable with Coq?<br>Date: Wed, 30 Dec 2015 02:44:23 +0100<br><br><div>I'm late, sorry, I just seen I received an answer.</div><div><br></div><div>On Tue, 29 Dec 2015 13:23:44 +0100, Ramana Kumar <ramana@member.fsf.org> wrote:<br></div><br><blockquote style="margin: 0 0 0.80ex; border-left: #0000FF 2px solid; padding-left: 1ex"><div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">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">
<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><div>You might be thinking of Holide. There is a link at <a href="http://dedukti.gforge.inria.fr/">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">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><div> </div></div></div></div></blockquote><div><br></div><div>Thanks for the pointers, I will follow these tracks later.</div><div><br></div><blockquote style="margin: 0 0 0.80ex; border-left: #0000FF 2px solid; padding-left: 1ex"><div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><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><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.</div></div></div></div></blockquote><div><br></div><div>I would be glad (modulo the time I could give it), just keep in mind I'm neither a professor nor even a student. I know HOL, and LCF intuitively, also a bit their history and how they are related (how LCF led to HOL) and know SML well enough. If you believe that's enough to be useful, then why not …</div><div><br></div><blockquote style="margin: 0 0 0.80ex; border-left: #0000FF 2px solid; padding-left: 1ex"><div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><div><br></div><div>Writing proofs in HOL4 or HOL Light is not as frightening as you might think :)</div></div></div></div></blockquote><div><br></div><div>Just started reading the HOL4 tutorial (I finally opted for HOL4 over HOL Light), I will see. I just though I may use a wrapper to be able so step forward and backward in a source, like CoqIDE do. If I do so, I will tell (oops, HOL4 related, not OpenTheory, I'm a bit out of topic).</div><div><br></div><blockquote style="margin: 0 0 0.80ex; border-left: #0000FF 2px solid; padding-left: 1ex"><div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><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><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></div></div></div></blockquote><div><br></div><div>I just can say the same as above: if you believe I'm able to, I may.</div><br><div id="M2Signature"><div>-- </div><div>Yannick Duchêne</div></div><br><br><br><div id="M2Signature"><div>-- </div><div>Yannick Duchêne</div></div></body></html>