[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
===================================================================
RocqPL 2026
12th International Workshop on Rocq
for Programming Languages
--
January 17, 2026, co-located with POPL
Rennes, France
CALL FOR PRESENTATIONS
https://urldefense.com/v3/__https://popl26.sigplan.org/home/rocqpl-2026__;!!IBzWLUs!TxdqRA6grcVf0HOUf8Li9M6nfK-wOXb3SAkUE_frNm9--KGtB2PpL69N0RcVVfQ8324Lvc1infFxsCSzBdezhdbrs4zjlaw$
===================================================================
Workshop Overview
-----------------
The series of RocqPL (formerly CoqPL[^1]) workshops provide an opportunity for
programming languages researchers and practitioners with an interest in Rocq 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.
[^1] The Coq theorem prover officially changed its name to the Rocq theorem
prover in March 2025; we have updated the name of the workshop from CoqPL to
RocqPL to reflect this change.
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 proof assistant
- 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://urldefense.com/v3/__https://rocqpl26.hotcrp.com/__;!!IBzWLUs!TxdqRA6grcVf0HOUf8Li9M6nfK-wOXb3SAkUE_frNm9--KGtB2PpL69N0RcVVfQ8324Lvc1infFxsCSzBdezhdbrTa6VYQk$
Important Dates:
- Submission: Friday, October 24, 2025
- Notification: Friday, November 21, 2025
- Workshop: Saturday, January 17, 2026
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://urldefense.com/v3/__https://www.sigplan.org/Resources/Author__;!!IBzWLUs!TxdqRA6grcVf0HOUf8Li9M6nfK-wOXb3SAkUE_frNm9--KGtB2PpL69N0RcVVfQ8324Lvc1infFxsCSzBdezhdbr_YGDUdg$
.
Program Committee
-----------------
Co-chairs:
- Benjamin Delaware, Purdue University, United States
- Frédéric Besson, Inria Rennes, France
Program Committee:
- Arthur Azevedo de Amorim, Rochester Institute of Technology, United States
- François Pottier, Inria, France
- Kiran Gopinathan, University of Illinois, Urbana Champaign, United States
- Samuel Gruetter, ETH Zurich, Switzerland
- Swarn Priya, Virginia Tech, United States
- Talia Ringer, University of Illinois Urbana-Champaign, United States
- Thomas Bourgeat, EPFL, Switzerland
- Yizhou Zhang, University of Waterloo, Canada
