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)
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).