The Coq mailing list

[Ronan Saillard <ronan.saillard AT inria.fr>]

Dedukti is a proof checker/type checker for the lambda-Pi-calculus 
modulo. You can think of it as a LF (Logical Framework) + rewrite rules.
You can weaken the definitional equality by adding your own rewrite 
rules so that the conversion test is made modulo beta+'your rules'.
This formalism is powerful enough to encode many logics such as any 
functional PTS or the theory of Coq (we have a tool for that: CoqIne) or 
the theory of HOL (another tool: Holide).
Our opinion is that the use of rewrite rules allows to keep the 
computational part of the logic one encodes and to get shallower encodings.
As Pierre said we are currently studying how we can make interoperate 
different logics in this setting. More precisely we want to prove A=>B 
in Coq, A in HOL and being able to deduce B.

Our (not too much out-of-date) web page is indeed: 
https://www.rocq.inria.fr/deducteam/Dedukti/index.html

Ronan.


On 19/12/2012 19:58, Benoit Montagu wrote:
> 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