The Coq mailing list

[Pierre Boutry <boutry AT unistra.fr>]

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
---------------

21 July 2025 (AoE): Submission deadline (extended)

10 August 2025: Author notification

Submission instructions
-----------------------

Submissions should take the form of a two-page PDF (excluding bibliography) 
and must be performed on Easychair.

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/](https://coq-workshop.gitlab.io/2025/)

**Submission link:** 
[https://easychair.org/conferences/?conf=rocqws2025](https://easychair.org/conferences/?conf=rocqws2025)

Program committee
-----------------

*   Aurèle Barrière (EPFL)
*   Sylvie Boldo (Inria Saclay)
*   Pierre Boutry (University of Strasbourg) [chair]
*   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) [chair]
*   June Rousseau (Aarhus University)
*   Natalia Ślusarz (Heriot-Watt University)
*   Nicolas Tabareau (Inria Rennes)
*   Quentin Vermande (Inria Sophia)

Organisers and contact
----------------------

*   Pierre Boutry
*   Loïc Pujet
*   [rocqws2025 AT easychair.org](mailto:rocqws2025 AT easychair.org)