License
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2011.21
URN: urn:nbn:de:0030-drops-31192
URL: http://drops.dagstuhl.de/opus/volltexte/2011/3119/
Go to the corresponding LIPIcs Volume Portal


Contejean, Évelyne ; Courtieu, Pierre ; Forest, Julien ; Pons, Olivier ; Urbain, Xavier

Automated Certified Proofs with CiME3

pdf-format:
Document 1.pdf (543 KB)


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 skeptical 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.

BibTeX - Entry

@InProceedings{contejean_et_al:LIPIcs:2011:3119,
  author =	{{\'E}velyne Contejean and Pierre Courtieu and Julien Forest and Olivier Pons and Xavier Urbain},
  title =	{{Automated Certified Proofs with CiME3}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{21--30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9 },
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Manfred Schmidt-Schau{\ss}},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2011/3119},
  URN =		{urn:nbn:de:0030-drops-31192},
  doi =		{http://dx.doi.org/10.4230/LIPIcs.RTA.2011.21},
  annote =	{Keywords: Rewriting, Formal Proof, Proof Automation, Proof Assistant}
}

Keywords: Rewriting, Formal Proof, Proof Automation, Proof Assistant
Seminar: 22nd International Conference on Rewriting Techniques and Applications (RTA'11)
Issue Date: 2011
Date of publication: 26.04.2011


DROPS-Home | Fulltext Search | Imprint Published by LZI