RocqPL

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:

• Submissions for talks and demonstrations should be described in an extended abstract, between 1 and 2 pages in length (excluding bibliography).
• Submission page: https://rocqpl27.hotcrp.com/
• We suggest authors format their abstracts using the two-column ACM SIGPLAN latex style (9pt font); a template is available here.
• RocqPL 2027 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.