[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


@techreport {
title="{Automated Certified Proofs with CiME3}",
author="E. Contejean and P. Courtieu and J. Forest and O. Pons and X. Urbain",
institution="{CEDRIC laboratory, CNAM-Paris, France}",