[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
The 1st Coq Workshop ==================== (http://coq.inria.fr/coq-workshop) 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 Venue: TPHOLs 2009, Munich, Germany Important Dates: * Papers Due: May 11, 2009 (* New deadline *) * Acceptance Notification: June 23, 2009 * Workshop: August 21, 2009 Program committee: * Yves Bertot * Frédéric Blanqui * Jacek Chrząszcz * Eduardo Giménez * Georges Gonthier * Hugo Herbelin (chair) * Greg Morrisett * David Nowak * Benjamin Pierce Authors should send their papers to hugo.herbe...@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 or letter 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.