===================================================================
RocqPL 2027
13th International Workshop on Rocq
for Programming Languages
--
January 16, 2027, co-located with POPL
Mexico City, Mexico
CALL FOR PRESENTATIONS
https://popl27.sigplan.org/home/rocqpl-2027
===================================================================
Workshop Overview
The series of RocqPL (formerly CoqPL) workshops provide an opportunity for programming languages researchers and practitioners with an interest in the Rocq Prover to meet and interact with one another and members from the core Rocq development team. At the meeting, we will discuss upcoming new features, see talks and demonstrations of exciting current projects, solicit feedback for potential future changes to Rocq itself, and generally work to strengthen the vibrant community around our favorite proof assistant.
Topics in scope include:
- Formalizations of PL 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
Workshop Format
The workshop format will be driven by you, the members of the community. We will solicit abstracts for talks and proposals for demonstrations and flesh out format details based on responses. We expect the final program to include experiment reports, panel discussions, and invited talks (details TBA). Talks will be selected according to relevance to the workshop, based on the submission of an extended abstract.
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://rocqpl27.hotcrp.com/
Important Dates:
- Submission: Friday, October 23, 2026
- Notification: Friday, November 20, 2026
- Workshop: Saturday, January 16, 2027
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: Author Information. We can accommodate remote talks under exceptional circumstances (for example, visa issues), but we expect that otherwise all talks should be in person.
Program Committee
Co-chairs:
- Arthur Azevedo de Amorim, Rochester Institute of Technology, United States
- Frédéric Besson, Inria Rennes, France
Program Committee:
- Ariel Eileen Kellison, Code Metal, Inc
- Benedikt Ahrens, Delft University of Technology, Netherlands
- Beta Ziliani, Universidad ORT, Uruguay
- Ike Mulder, Radboud University Nijmegen, Netherlands
- Karl Palmskog, KTH Royal Institute of Technology, Sweden
- Lourdes de Carmen González Huesca, National Autonomous University of Mexico, Mexico
- Steve Zdancevic, University of Pennsylvania, United States
- Zoe Paraskevopoulou, National Technical University of Athens, Greece