[CCF11a] Automated Certified Proofs with CiME 3

Conférence Internationale avec comité de lecture : 22nd Int. Conf. on Rewriting Techniques and Applications, May 2011, Vol. 10, pp.21-30, Series LIPIcs, Novi Sad, Serbie,

Auteurs: E. Contejean , P. Courtieu , J. Forest , O. Pons , X. Urbain

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

@inproceedings {
	CCF11a,
	title	=	"{Automated Certified Proofs with CiME 3}",
	author	=	" E. Contejean and P. Courtieu and J. Forest and O. Pons and X. Urbain ",
	booktitle	=	"{22nd Int. Conf. on Rewriting Techniques and Applications}",
	year	=	2011,
	month	=	"May",
	series	=	"LIPIcs",
	volume	=	10,
	pages	=	"21-30",
	address	=	"Novi Sad, Serbie",
}