The goal of this workshop is to provide an opportunity for programming languages researchers and practitioners with an interest in the Rocq Prover to meet and interact with one another and with members of the core Rocq development team. At the meeting, we will discuss upcoming new features, see talks and demonstrations of active projects, solicit feedback for potential future work on Rocq itself, and generally work to strengthen the vibrant community around our favorite proof assistant.
Topics in scope include:
- Formalizations of programming language research in Rocq
- General purpose libraries and tactic language extensions
- Domain-specific libraries for programming language formalization and verification
- IDEs, profilers, tracers, debuggers, and testing tools
- Reports on ongoing proof efforts conducted via (or in the context of) the Rocq Prover
- Experience reports from Rocq usage in educational or industrial contexts
To foster open discussion of cutting edge research which can later be published in full conference proceedings, we will not publish papers from the workshop.
Plenary
This program is tentative and subject to change.
Sat 17 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Sat 17 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
09:00 - 10:30 | |||
09:00 45mKeynote | Future-Proofing Numerical Accuracy with Formal Specifications RocqPL Ariel E. Kellison Cornell University | ||
09:45 15mTalk | Crane Lowers Rocq Safely into C++ RocqPL | ||
10:00 15mTalk | Specifying and Verifying the NOVA Microhypervisor in Concurrent Separation Logic RocqPL | ||
10:15 15mTalk | The HOL-Light library of Multivariate real analysis in Rocq RocqPL | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break POPL Catering | ||
11:00 - 12:30 | |||
11:00 45mPanel | Session with the Rocq Development Team RocqPL | ||
11:45 15mTalk | Rocq CARVe-ing: A Library for Substructural Meta-Theory RocqPL Daniel Zackon McGill University, Ryan Kavanagh Université du Québec à Montréal, Alberto Momigliano Università degli Studi di Milano, Brigitte Pientka McGill University | ||
12:00 15mTalk | Scalable Type Inference for Intrinsically-Typed Binders RocqPL Max Kurze Barkhausen Institut, Clément Pit-Claudel EPFL, Sebastian Ertel Barkhausen Institute, Dresden | ||
12:15 15mTalk | Sulfur: Substitution Generation using a Logical Framework RocqPL Mathis Bouverot-Dupuis INRIA & École Normale Supérieure, Théo Winterhalter INRIA, Kenji Maillard Inria, Kathrin Stark Heriot-Watt University | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch POPL Catering | ||
14:00 - 15:30 | |||
14:00 15mTalk | A systematic approach to "Well-founded recursion done right" RocqPL Herman Geuvers Radboud University Nijmegen, Netherlands, Gijs Pennings Eindhoven University of Technology | ||
14:15 15mTalk | Implementing parametricity in Rocq-ELPI RocqPL | ||
14:30 15mTalk | Mechanically Verified Universe Checking and Variance Inference for The Rocq Prover RocqPL | ||
14:45 15mTalk | Nested Inductive Types for Rocq and Lean RocqPL Thomas Lamiaux Nantes Université, Inria, Yannick Forster INRIA, Matthieu Sozeau Inria, Nicolas Tabareau Inria | ||
15:00 15mTalk | Trocq parametricity translations for inductives RocqPL Tomas Vallejos Parada Inria | ||
15:15 15mTalk | Verifying Synchronous Dataflow Programs with SMTCoq RocqPL Basile Pesin Ecole Nationale de l'Aviation Civile (ENAC) | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break POPL Catering | ||
Accepted Papers
Call for Presentations
To foster open discussion of cutting edge research which can later be published in full conference proceedings, we will not publish papers from the workshop. However, presentations may be recorded and the videos may be made publicly available.
Submission Details:
- Submissions for talks and demonstrations should be described in an extended abstract, between 1 and 2 pages in length (excluding bibliography).
- Submission page: https://rocqpl26.hotcrp.com/
- We suggest authors format their abstracts using the two-column ACM SIGPLAN latex style (9pt font); a template is available here.
- RocqPL 2026 will use a single-blind reviewing process, so submissions will not be anonymous.
- HotCRP will ask authors for a short abstract when uploading their submissions; these summaries will eventually be included in the program on the conference website. These summaries are not required to be included in extended abstracts, but authors are free to do so if they want.
Important Dates:
- Submission: Friday, Oct 24, 2025 (AoE)
- Notification: Friday, November 21, 2025
- Workshop: Saturday, January 17, 2025
Important Dates AoE (UTC-12h)
| Sat 17 Jan 2026 RocqPL Workshop |
| Fri 28 Nov 2025 Notification |
| Fri 31 Oct 2025 Submission Deadline |
Submission Link
Arthur Azevedo de Amorim
Rochester Institute of Technology
United States
Thomas Bourgeat
EPFL
Switzerland
Kiran Gopinathan
Basis
United States
Samuel Gruetter
ETH Zurich
François Pottier
Inria
France
Swarn Priya
Virginia Tech
United States
Talia Ringer
University of Illinois at Urbana-Champaign
United States
Yizhou Zhang
University of Waterloo
Canada