[opentheory-users] Fwd: Re: Is OpenTheory usable with Coq?

[Yannick]

------- Forwarded message -------
From: Yannick <yannick_duchene at yahoo.fr>
To: "Ramana Kumar" <ramana at member.fsf.org>
Cc:
Subject: Re: [opentheory-users] Is OpenTheory usable with Coq?
Date: Wed, 30 Dec 2015 02:44:23 +0100

I'm late, sorry, I just seen I received an answer.

On Tue, 29 Dec 2015 13:23:44 +0100, 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).
>

Thanks for the pointers, I will follow these tracks later.

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

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 …

>
> Writing proofs in HOL4 or HOL Light is not as frightening as you might  
> think :)

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

>
>>
>> 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 just can say the same as above: if you believe I'm able to, I may.

-- 
Yannick Duchêne



-- 
Yannick Duchêne
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20151230/2a308d81/attachment-0001.html>