Automated Certified Proofs with CiME3

Evelyne Contejean 1, 2 Pierre Courtieu 3 Julien Forest 4 Olivier Pons 3 Xavier Urbain 1, 2
1 LRI - Laboratoire de Recherche en Informatique
2 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
3 CEDRIC - Centre d'étude et de recherche en informatique et communications
4 Artenum, Paris
Abstract : We present the rewriting toolkit CiME3. Amongst other original features, this version enjoys two kinds of engines: to handle and discover proofs of various properties of rewriting systems, and to generate Coq scripts from proof traces given in certification problem format in order to certify them with a sceptical proof assistant like Coq. Thus, these features open the way for using CiME3 to add automation to proofs of termination or confluence in a formal development in the Coq proof assistant.
Type de document :
Communication dans un congrès
RTA - 22nd International Conference on Rewriting Techniques and Applications, 2011, Novi Sad, Serbia. 2011
Liste complète des métadonnées
https://hal.inria.fr/hal-00777669
Contributeur : Claude Marché <>
Soumis le : jeudi 17 janvier 2013 - 17:24:14
Dernière modification le : vendredi 12 octobre 2018 - 15:04:06

Identifiants

  • HAL Id : hal-00777669, version 1

Collections

INRIA | UMR8623 | LRI-VALS | UNIV-HESAM

Citation

Evelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, Xavier Urbain. Automated Certified Proofs with CiME3. RTA - 22nd International Conference on Rewriting Techniques and Applications, 2011, Novi Sad, Serbia. 2011. 〈hal-00777669〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

206

Contact


archive-ouverte@inria.fr