The Coq mailing list

[stvienna wiener <stvienna AT gmail.com>]

Hi all,

Where can I start looking about the state of the art of automation in Coq? I have read that there is ongoing work on SMT/SAT integration, as well as automation support for resolution and rewriting proofs.

Are there any current papers I should look at?

By “Coq automation”, I mean automation regarding resolution, rewriting and SAT/SMT solver integration. I am less interested in the basic automation tools (auto, trivial or omega).

So far I have looked at the Coq workshop, ITP and the issues Journal of Automated reasoning for the last six years. I am aware that my question is rather broad and I still have some literature research to do. However, I would be glad if I get pointers into the right direction.

Best regards from Vienna,

Steve

PS: these are the papers I found so far:

[1] Armand, Michaël, et al. "A modular integration of SAT/SMT solvers to Coq through proof witnesses." Certified Programs and Proofs. Springer Berlin Heidelberg, 2011. 135-150.

[2] Blanqui, Frédéric, and Adam Koprowski. "CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates." Mathematical Structures in Computer Science 21.04 (2011): 827-859.

[3] Strub, Pierre-Yves. "Coq modulo theory." Computer Science Logic. Springer Berlin Heidelberg, 2010.

[4] Boldo, Sylvie, Jean-Christophe Filliâtre, and Guillaume Melquiond. "Combining Coq and Gappa for certifying floating-point programs." Intelligent Computer Mathematics. Springer Berlin Heidelberg, 2009. 59-74.

[5] Bezem, Marc, Dimitri Hendriks, and Hans De Nivelle. "Automated proof construction in type theory using resolution." Journal of Automated Reasoning 29.3 (2002): 253-275.