POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France

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.

Accepted Papers

Title
Abstract VCG: Tie-breaking rules in VCG mechanism design
RocqPL
A systematic approach to "Well-founded recursion done right"
RocqPL
Crane Lowers Rocq Safely into C++
RocqPL
Formal Assurance for Railway Interlockings: Verifying Z3 SAT Proofs with Tseitin in Rocq
RocqPL
Formalizing a First-order Differentiable Logic with MathComp
RocqPL
Implementing parametricity in Rocq-ELPI
RocqPL
Lambda JS à la Carte
RocqPL
Mechanically Verified Universe Checking and Variance Inference for The Rocq Prover
RocqPL
Nested Inductive Types for Rocq and Lean
RocqPL
Recursive Mutexes in Separation Logic
RocqPL
Rocq CARVe-ing: A Library for Substructural Meta-Theory
RocqPL
Scalable Type Inference for Intrinsically-Typed Binders
RocqPL
Specifying and Verifying the NOVA Microhypervisor in Concurrent Separation Logic
RocqPL
Sulfur: Substitution Generation using a Logical Framework
RocqPL
The HOL-Light library of Multivariate real analysis in Rocq
RocqPL
Towards a Mechanization of the ECMAScript (JavaScript) Proposal "Temporal"
RocqPL
Trocq parametricity translations for inductives
RocqPL
Verification of Templated Code in C++
RocqPL
Verifying Synchronous Dataflow Programs with SMTCoq
RocqPL

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