[Termtools] CeTA: a stand-alone termination proof certifier

[Adam Koprowski]

   Dear Innsbruck-ppl,

  I'd like to add my congratulations to those of Frederic. Using extraction
sounds like an excellent idea to me and your experimental results absolutely
confirm that this is the way to go. Well done!

  This of course creates a new issue for the termination competition: the
rules for admitting tools to the certified category will have to be changed
if we are to allow extracted programs to run in this category (and we
should).

   Cheers,
   Adam

2009/3/22 Frederic Blanqui <frederic.blanqui at inria.fr>

> Congratulations! It is a very good idea to use an extracted program. It
> allows you to get round the slowness of proof assistants. We did not do
> that with Rainbow and CoLoR yet but it should not be too difficult to do
> it (Coq also has this feature). I will try to do that soon too ;-) Best
> regards, Frederic.
>
> René Thiemann a écrit :
> > Dear all,
> >
> > we are happy to announce IsaFoR and CeTA which are both freely
> > available at:
> >
> >    http://cl-informatik.uibk.ac.at/software/ceta/
> >
> > * IsaFoR (Isabelle Formalization of Rewriting) is an Isabelle/HOL
> >    library which formalizes first order term rewriting.
> >    It currently contains several definitions, theorems, and
> >    algorithms about rewriting, where the main focus is on
> >    termination analysis.
> >
> >    - terms, TRSs, matching, unification
> >    - dependency pairs (incl. dependency pair framework)
> >    - dependency graph processor (EDG***, i.e., EDG* with tcap)
> >    - reduction pair processor
> >    - polynomial orders
> >    - nontermination via loops
> >    - ...
> >
> >    For each of the termination techniques, IsaFoR contains a check-
> > function
> >    which--given a termination proof from an arbitrary termination
> >    prover--checks whether these techniques have been applied in a
> > correct
> >    way. Hence, these functions can be used to certify termination proof
> >    trees.
> >
> > * Since all our check-functions are executable, we used Isabelle's
> >    code-generation facilities to generate a certified Haskell program,
> >    CeTA (Certified Termination Analysis), which can then also be used
> >    to certify termination proof trees. It has the following benefits:
> >
> >    - readable error messages in case a proof tree is refuted
> >    - execution time: certification of over 500 proofs in 1 minute
> >    - robustness: any dependency graph estimation is accepted,
> >                  as long as it is subsumed by EDG***
> >    - modularity: for each termination technique one can call an
> > individual
> >               check-function, the whole proof tree is not required
> >    - easy usage: just download a binary or some Haskell-files,
> >                  an installation of Isabelle is not required;
> >                  simple proof tree format
> >
> > * For the future we have the following plans:
> >    - subterm criterion
> >    - negative polynomial orders
> >    - combination with other termination proof certifiers via common
> >      XML proof tree format (we aim for some results after WST'09)
> >    - submission to the archive of formal proofs
> >    - ...
> >
> > So stay tuned.
> >
> > Best regards,
> > Christian Sternagel,
> > René Thiemann, and
> > Harald Zankl
> > _______________________________________________
> > Termtools mailing list
> > Termtools at lists.lri.fr
> > http://lists.lri.fr/mailman/listinfo/termtools
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/mailman/listinfo/termtools
>



-- 
=====================================================
Adam.Koprowski at gmail.com, http://www.cs.ru.nl/~Adam.Koprowski
The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.lri.fr/pipermail/termtools/attachments/20090322/715718eb/attachment.htm