The 4th Coq Workshop
Princeton, NJ, USA
August 12, 2012
(A satellite workshop of ITP 2012)
The Coq Workshop series brings together Coq users, developers, and contributors. While conferences like ITP provide a venue for traditional research papers, the Coq Workshop focuses on strengthening the Coq community and providing a forum for discussing practical issues, including the future of the Coq software and its associated ecosystem of libraries and tools. Thus, the workshop will be organized around informal presentations and discussions, supplemented with invited talks.
Submission Instructions (expired)
We invite all members of the Coq community to propose informal talks, discussion sessions, or any potential uses of the day allocated to the workshop. Relevant subject matter includes but is not limited to:
- Language or tactic features
- Theory and implementation of the Calculus of Inductive Constructions
- Applications and experience in education and industry
- Tools and platforms built on Coq
- Plugins and libraries for Coq
- Interfacing with Coq
- Formalization tricks and Coq pearls
Authors should submit short proposals through EasyChair. Submissions should be in portable document format (PDF). Proposals should not exceed 2 pages in length in single-column full-page style.
This year, we are open to many ideas on how to use the workshop time. Some suggestions to drive proposals include sessions on tool demonstrations or lessons learned from teaching Coq.
- June 1: Deadline for proposal submission
- June 15: Acceptance notification
- August 12: Workshop in Princeton
- Yves Bertot, INRIA, France
- Arthur Charguéraud, MPI-SWS, Germany
- Adam Chlipala (chair), MIT, USA
- Chung-Kil Hur, MPI-SWS, Germany
- Assia Mahboubi, INRIA, France
- Zhong Shao, Yale, USA
- Bas Spitters, Nijmegen, Netherlands
- Jean-Baptiste Tristan, Oracle, USA
- Vladimir Voevodsky, IAS, USA
For More Information
E-mail Adam Chlipala
The workshop is supported by the Coq Technological Development Action (at INRIA).