The Coq workshop brings together Coq users, developers and contributors. In 2010, it contains contributed papers and informal presentations on usages and the evolution of the Coq system (see the call for paper). It is held in Edinburgh, on July 9, as a satellite workshop of the ITP conference and a part of the Federated Logic Conference.

The proceedings of the workshop contain two refereed papers.

Program
09:00-09:30 Inductive Proof Automation for Coq Sean Wilson, Jacques Fleuriot, Alan Smaill
09:30-10:00 Heq: A Coq library for Heterogeneous Equality Chung-Kil Hur
10:00-10:30 break
10:30-11:00 Proof Trick: small Inversions Jean-François Monin
11:00-11:30 Strengthening the inversion Tactic in Coq Anne Mulhern
11:30-12:00 Mixed induction-coinduction at work for Coq Keiko Nakata and Tarmo Uustalu
12:00-12:30 Certification of a chain for deductive program verification Paolo Herms
12:30-14:00 Lunch break
14:00-14:30 Recent evolutions in the Coq system Hugo Herbelin
14:30-15:00 Rewriting Modulo Associativity and Commutativity Thomas Braibant and Damien Pous
15:00-15:30 break
15:30-16:00 Developing the algebraic hierarchy with type classes in Coq Bas Spitters and Eelis van der Wegen
16:00-16:30 Experience of interfacing Coq+SSReflect and GAP Vladimir Komendantsky, Alexander Konovalov and Steve Linton
16:30-17:00 Root isolation for one-variable polynomials Yves Bertot and Assia Mahboubi

The workshop is supported by the Coq Technological Development Action (at INRIA).