CfC: The Rocqshop 2026

1ST CALL FOR CONTRIBUTIONS AND PARTICIPATION

The Rocqshop 2026

25 July 2026 (*), Lisbon, Portugal. Part of FLoC 2026.
https://coq-workshop.gitlab.io/2026/

The Rocqshop (formerly the Coq Workshop) brings together users, developers, and contributors of the Rocq prover. While conferences like ITP provide a venue for traditional research papers, 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, the Rocqshop will be organised around informal presentations and discussions, supplemented with invited talks. We invite all members of the Rocq community to propose informal talks, discussion sessions, or any other potential use 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 Rocq

  • Plugins and libraries for Rocq

  • Interfacing with Rocq

  • Formalisation tricks and Rocq pearls

Considering the broad background of the expected audience, we encourage authors to include pedagogical information.

Schedule

  • Abstract submission deadline: May 15

  • Author notification: June 15

  • Workshop: July 25 (due to scheduling issues, the date on the FLoC website was wrong until today)

Submissions should consist of a title and a 1-2 pages abstract not including references, in pdf format, via https://submissions.floc26.org/rocqws/paper/new . Indicate the intended speaker in the abstract by bolding their name.

Program committee

See https://coq-workshop.gitlab.io/2026/ .

Organizers