Automated Certified Proofs with CiME3 - Archive ouverte HAL Access content directly
Conference Papers Year : 2011

Automated Certified Proofs with CiME3

(1, 2) , (3) , (4) , (3) , (1, 2)
1
2
3
4

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 sceptical 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.
Not file

Dates and versions

hal-00777669 , version 1 (17-01-2013)

Identifiers

  • HAL Id : hal-00777669 , version 1

Cite

Evelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, Xavier Urbain. Automated Certified Proofs with CiME3. RTA - 22nd International Conference on Rewriting Techniques and Applications, 2011, Novi Sad, Serbia. ⟨hal-00777669⟩
131 View
0 Download

Share

Gmail Facebook Twitter LinkedIn More