The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

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.

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