LIPIcs.RTA.2011.21.pdf
- Filesize: 0.53 MB
- 10 pages
Document
Automated Certified Proofs with CiME3
Authors
-
Part of:
Volume:
22nd International Conference on Rewriting Techniques and Applications (RTA'11) (RTA 2011)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Rewriting Techniques and Applications (RTA) - License:
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
- Publication Date: 2011-04-26
Cite AsGet BibTex
Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Automated Certified Proofs with CiME3. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 21-30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
https://doi.org/10.4230/LIPIcs.RTA.2011.21
https://doi.org/10.4230/LIPIcs.RTA.2011.21
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.
Keywords
- Rewriting
- Formal Proof
- Proof Automation
- Proof Assistant
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads