The Coq mailing list

[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