The Coq Proof Assistant

 
A Tactic for Deciding Kleene Algebras Thomas Braibant - Damien Pous
A New Look at Generalized Rewriting in Type Theory Matthieu Sozeau
Descente Infinie Proofs in Coq Răzvan Voicu - Mengran Li
Sets in Coq, Coq in Sets Bruno Barras
Formalizing a SAT Checker in Coq Ashish Darbari - Bernd Fischer - Joao Marques-Silva
Proof Objects for Logical Translations Andrew Polonsky - Marc Bezem