We are pleased to invite you to submit presentation proposals for the Rocqshop 2025 (formerly the Coq Workshop), which will be held in Reykjavik, Iceland on 27 September 2025, as a satellite to the ITP conference.
The Rocqshop 2025 is the 16th instalment of the Coq Workshop series. The workshop brings together developers, contributors, and users of the Rocq Prover.
The Rocqshop focuses on strengthening the Rocq community and providing a forum for discussing practical issues, including the future of the Rocq Prover and its associated ecosystem of libraries and tools. Thus, rather than serving as a venue for traditional research papers, the Rocqshop is organised around informal presentations and discussions, supplemented with invited talks.
Important dates
13 July 2025 (AoE): Submission deadline (a deadline extension is likely)
10 August 2025: Author notification
Submission instructions
Submissions should take the form of a two-page PDF (excluding bibliography). A link to the submission platform will be added soon.
You have the freedom to produce the PDF by whatever means but keep in mind that it should remain legible for the people of the PC and for attendees of the conference so please avoid two pages of text with absolutely no margin.
We use a single-blind review process, meaning that reviewers have access to the identity and affiliations of the authors. As such, the submitted PDF should include name and affiliations in addition to the title and abstract.
Relevant subject matter includes but is not limited to:
- Language or tactic features for Rocq
- Theory and implementation of the Calculus of Inductive Constructions
- Applications of Rocq and experience reports on Rocq use in education and industry
- Tools and platforms built on Rocq
- Plugins and libraries for Rocq
- Interfacing with Rocq
- Formalisation tricks and Rocq pearls
Workshop website: https://coq-workshop.gitlab.io/2025/
Program committee (under construction)
- Aurèle Barrière (EPFL)
- Sylvie Boldo (Inria Saclay)
- Pierre Boutry (University of Strasbourg)
- Hugo Herbelin (Inria Paris)
- Axel Ljungström (Stockholm University)
- Hannah Leung (University of Illinois)
- Jade Philipoom (zeroRISC)
- Swarn Priya (Virginia Tech)
- Loïc Pujet (Stockholm University)
- Natalia Ślusarz (Heriot-Watt University)
- Nicolas Tabareau (Inria Rennes)
- Quentin Vermande (Inria Sophia)
Organisers and contact
- Pierre Boutry
- Loïc Pujet