Coq-2 Accepted Papers

Proof Trick: Small Inversions
Inductive Proof Automation for Coq
Developing the algebraic hierarchy with type classes in Coq
Experience of interfacing Coq+SSReflect and GAP
Root isolation for one-variable polynomials
Rewriting Modulo Associativity and Commutativity
Certification of a chain for deductive program verification
Heq: A Coq library for Heterogeneous Equality
Mixed induction-coinduction at work for Coq
Strengthening the inversion Tactic in Coq