Email Gateway (Aug 18 2022 at 13:13): Email Gateway (Aug 18 2022 at 13:13):From: René Thiemann <rene.thiemann@uibk.ac.at>
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.
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:
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:
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
Last updated: May 03 2024 at 04:19 UTC