The Coq mailing list

[Pierre-Yves Strub <pierre-yves AT strub.nu>]

Hi,

The webpage is back, but the implementation if out of date (for Coq
8.3pl3) and I don't plan to update it.

Best,
-- Pierre-Yves.

2015-04-29 17:39 GMT+02:00 Jonathan Leivent 
<jonikelee AT gmail.com>:
>
>
> On 04/29/2015 11:08 AM, Frédéric Blanqui wrote:
>>
>> Jonathan, you may be interested by CoqMT developed by Pierre-Yves Strub.
>> See http://www.strub.nu/coqmt . Unfortunately, this website does not seem
>> accessible for the moment. Best regards, Frédéric.
>
>
> Thanks, Frédéric.   I found this paper:
> https://hal.inria.fr/file/index/docid/497404/filename/csl-2010.pdf
>
> -- Jonathan
>
>
>
>>
>> Le 29/04/2015 16:48, Jonathan Leivent a écrit :
>>>
>>>
>>>
>>> On 04/29/2015 10:09 AM, David MENTRE wrote:
>>>>
>>>> Hello,
>>>>
>>>> Le 29/04/2015 15:53, Jonathan Leivent a écrit :
>>>>>
>>>>> On 04/28/2015 03:37 PM, Evelyne Contejean wrote:
>>>>>>
>>>>>> There is also the "ergo" tactic, due to Stéphane Lescuyer, as a part
>>>>>> of his thesis when he was a PhD student of mine.
>>>>>>
>>>>>> www.lix.polytechnique.fr/coq/pylons/.../Ergo/v8.3
>>>>>
>>>>>
>>>>> I get a "404 Not Found" error for that link.
>>>>
>>>>
>>>> Following URL is working (found with Google):
>>>>
>>>>
>>>> http://www.lix.polytechnique.fr/coq/pylons/contribs/files/Ergo/v8.4/Ergo.tar.gz
>>>>
>>>> Best regards,
>>>> david
>>>>
>>>
>>> I found the description here:
>>>
>>> http://www.lix.polytechnique.fr/coq/pylons/contribs/view/Ergo/trunk
>>>
>>> which says "This extension is limited to non-dependent types." - are
>>> there any SMT solvers that can work with dependent types?
>>>
>>>
>>> But, regardless...
>>>
>>> The ability to link to SMT solvers and use them as decision procedures is
>>> certainly interesting and helpful - but I was hoping for a different kind 
>>> of
>>> synergy between SMT and Coq - that would perhaps allow Coq to achieve a 
>>> more
>>> comprehensive proof search capability over any dependently-typed theory by
>>> using approaches that SMT solvers use to build and test alternative models
>>> for the existential variables tying together multiple subgoals.
>>>
>>> -- Jonathan
>>>
>>
>