The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

I guess you're not interested in tactic languages and the like. If you do, here are some pointers:

Rtac:
https://gmalecha.github.io/publication/2015/01/18/rtac-a-fully-reflective-tactic-language.html

Mtac:
http://plv.mpi-sws.org/mtac/

Proof by reflection:
Lightweight proof by reflection using a posteriori simulation of effectful computation.
G. Clauret, L. del C. González Huesca, Y. Régis-Gianas, B. Ziliani
In Conference on Interactive Theorem Proving (ITP 2013)

On Fri, May 15, 2015 at 3:57 AM, stvienna wiener <stvienna AT gmail.com> wrote:

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.