The Coq workshop 2009

Call for papers

The Coq workshop will bring together Coq users, developers and
contributors. The workshop will be organized from submitted papers,
invited talks and a plenary discussion on the evolution and design of
Coq. Topics for submitting a paper include:

  • Language or tactics features
  • Theory and implementation of the Calculus of Inductive Constructions
  • Applications and experience in education and industry
  • Tools, platforms built on Coq
  • Plugins, libraries for Coq
  • Interfacing with Coq
  • Formalization tricks and Coq pearls

Authors should send their papers to Hugo.Herbelin@inria.fr. Submitted
papers should be in (postscript or) portable document format. Papers
should not exceed 12 pages in length in single-column full-page 11pt A4
style.

If there is sufficient demand, we will try to organize a time slot for
demonstrations. Similarly, we may also organize a session on the lessons
learned from teaching Coq. If you are interested, please send a brief
proposal.

Venue:

TPHOLs 2009, Munich, Germany

Important Dates:

  • Papers Due: May 11, 2009
  • Acceptance Notification: June 23, 2009
  • Workshop: August 21, 2009

Program committee:

  • Yves Bertot
  • Frédéric Blanqui
  • Jacek Chrzączsz
  • Eduardo Giménez
  • Georges Gonthier
  • Hugo Herbelin (chair)
  • Greg Morrisett
  • David Nowak
  • Benjamin Pierce