The Coq mailing list

[Victor Porton <porton AT narod.ru>]

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

-- 
Victor Porton - http://portonvictor.org