The Second Coq Workshop was held in Edinburgh, Scotland, on July 9th, 2010,
as part of the Federated Logic Conference
(A satellite workshop of ITP 2010)
The
Coq workshop series 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. It was held in Edinburgh, on July 9, as a satellite workshop of the ITP conference and a part of the Federated Logic Conference.
Program committee
- Andrew Appel
- Yves Bertot (Chair)
- Adam Chlipala
- Georges Gonthier
- Benjamin Grégoire
- Hugo Herbelin
- Micaela Mayero
- Christine Paulin-Mohring
- Bas Spitters
Program
- Inductive Proof Automation for Coq, Sean Wilson, Jacques Fleuriot, Alan Smaill
- Heq: A Coq library for Heterogeneous Equality, Chung-Kil Hur
- Proof Trick: small Inversions, Jean-François Monin
- Strengthening the inversion Tactic in Coq>, Anne Mulhern
- Mixed induction-coinduction at work for Coq, Keiko Nakata and Tarmo Uustalu
- Certification of a chain for deductive program verification, Paolo Herms
- TBA, Hugo Herbelin
- Rewriting Modulo Associativity and Commutativity, Thomas Braibant and Damien Pous
- Developing the algebraic hierarchy with type classes in Coq, Bas Spitters and Eelis van der Wegen
- Experience of interfacing Coq+SSReflect and GAP, Vladimir Komendantsky, Alexander Konovalov and Steve Linton
- Root isolation for one-variable polynomials, Yves Bertot and Assia Mahboubi
The workshop was supported by the Coq Technological Development Action (at INRIA).
Réalisation Service IST INRIA Sophia Antipolis Méditerranée / Laboratoire I3S
