The Coq Proof Assistant

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