The goal of this workshop is to provide an opportunity for programming languages researchers and practitioners with an interest in Rocq 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 proof assistant
- 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.
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:
Submission page: https://rocqpl26.hotcrp.com/ (not active yet)
Important Dates:
- Submission: Friday, Oct 24, 2025 (AoE)
- Notification: Friday, November 21, 2025
- Workshop: Saturday, January 17, 2025
Submissions for talks and demonstrations should be described in an extended abstract, between 1 and 2 pages in length (excluding bibliography). We suggest formatting the text using the two-column ACM SIGPLAN latex style (9pt font). Templates are available from the ACM SIGPLAN page: https://www.sigplan.org/Resources/Author/.
| Fri 24 Oct 2025new Submission Deadline |
| Fri 21 Nov 2025new Notification |
| Sat 17 Jan 2026new RocqPL Workshop |
- No members yet