The Coq Workshop 2010

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:

  • Experiments with type-theoretic proof assistants
  • 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 submit their paper through EasyChair at the following link:

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.


FLoC 2010, Edinburgh, Scotland

Important Dates

  • March 22nd: Deadline for submission of papers
  • May 1st: Acceptance Notification
  • May 17th: Final version of articles
  • July 9th: Workshop in Edinburgh

Program Committee

  • Andrew Appel
  • Yves Bertot (Chair)
  • Adam Chlipala
  • Georges Gonthier
  • Benjamin GrĂ©goire
  • Hugo Herbelin
  • Micaela Mayero
  • Christine Paulin-Mohring
  • Bas Spitters