[TYPES/announce] [Cfp] Coq Workshop, Edinburgh, July 9, Program and call for participation

[Yves Bertot]

Dear Colleague,

Please consider attending the Federated Logic Conference (FLoC) and 
especially

   the Coq Workshop (Coq-2)
   Edinburgh, July 9th, 2010

The early registration deadline is May 17th.

    http://www.floc-conference.org
    http://coq.inria.fr/coq-workshop/2010

The Coq workshop will bring together Coq users, developers and 
contributors. It will be organized from submitted and refereed 
presentations and more informal presentations.  Please register and come 
participate in the discussions, even if you do not wish to submit any talks.

The workshop organizers

PROGRAM FOR THE COQ WORKSHOP
============================

Inductive Proof Automation for Coq

  by Sean Wilson, Jacques Fleuriot and Alan Smaill

Heq: A Coq library for Heterogeneous Equality

  by Chung-Kil Hur

Proof Trick: small Inversions

  by Jean-François Monin

Strengthening the inversion Tactic in Coq

  by anne mulhern

Mixed induction-coinduction at work for Coq

  by Keiko Nakata and Tarmo Uustalu

Certification of a chain for deductive program verification

  by Paolo Herms

Invited talk (title to be announced later)

  by Hugo Herbelin

Rewriting Modulo Associativity and Commutativity

  by Thomas Braibant and Damien Pous

Developing the algebraic hierarchy with type classes in Coq

  by Bas Spitters, Eelis van der Weegen

Experience of interfacing Coq+SSReflect and GAP

  by Vladimir Komendantsky, Alexander Konovalov and Steve Linton

Root isolation for one-variable polynomials

  by Yves Bertot and Assia Mahboubi