|
 
|
[CCF11] Automated Certified Proofs with CiME3
Rapport Scientifique : Date de dépot: 2011/02/01, Nb pages 11, (Tech. Rep.: CEDRIC-11-2044)Mots clés: Automated Proofs,Certified Proofs,rewriting,termination,confluence, proof assistant, Coq, CiME
Résumé:
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 proofs traces input in
Certification Proof Format (CPF) (an XML format widely
accepted by the certified rewriting community) in order to certify
them with a skeptical proof assistant like Coq. CiME3 may thus
be used to add automation to proofs of termination or confluence in
a formal development in the Coq proof assistant.
Equipe:
sys
BibTeX
| @techreport { | |||
| CCF11, | |||
| title | = | "{Automated Certified Proofs with CiME3}", | |
| author | = | "E. Contejean and P. Courtieu and J. Forest and O. Pons and X. Urbain", | |
| number | = | "{CEDRIC-11-2044}", | |
| institution | = | "{CEDRIC laboratory, CNAM-Paris, France}", | |
| date | = | {01-02-2011}, | |
| pages | = | "11", | |
| } | |||
