The Coq mailing list

[Benoit Montagu <benoit.montagu AT m4x.org>]

https://www.rocq.inria.fr/deducteam/Dedukti/

Le 19/12/2012 13:54, Victor Porton a écrit :
> 19.12.2012, 20:38, "Pierre Boutillier" 
> <pierre.boutillier AT pps.univ-paris-diderot.fr>:
> > We would like to use already proved theorems and not tackle the translation 
> > of these proofs in the logic in witch we will prove the next theorem. Going 
> > mechanically from one theory to an other is studied around Dedukti for 
> > example.
>
> http://www.lix.polytechnique.fr/dedukti/ does not load.
>
> There are no "Dedukti" article in Wikipedia.
>
> What is Dedukti?
>
> > >   Le 18 déc. 2012 à 22:23, Victor Porton 
> > > <porton AT narod.ru>
> > >  a écrit :
> > > >   I think that Coq is a VERY good proof assistant.
> > > >
> > > >   Nevertheless I dare to ask this question:
> > > >
> > > >   What will be the next generation of proof assistants? How and in which 
> > > > aspects they will surpass Coq?
> > > >
> > > >   --
> > > >   Victor Porton - http://portonvictor.org