RocqPL 2026
who it's for
Rocq contributors, theorem prover developers, formal methods engineers, verification engineers, programming language researchers, library and tooling maintainers
topics
parametricity translations for inductives; reflective tactic reification; well-founded recursion patterns; ECMAScript Temporal mechanization; Z3 RUP and Tseitin checking; NOVA microhypervisor verification; binary parametricity in ELPI; HOL-Light multivariate analysis port; algebraic universes and consistency checking; scalable type inference for intrinsically-typed binders; verification of templated C++ code; VCG tie-breaking formalization
| title | author | length |
|---|---|---|
| Sulfur: Substitution Generation using a Logical Framework | Mathis Bouverot-Dupuis, Théo Winterhalter, Kenji Maillard, Kathrin Stark | 15m |
A Coq/Rocq plugin reimplements Autosubst’s costly asimpl by reflective tactic reification: it generates concrete de Bruijn-based syntax, translates terms into… | ||
| A systematic approach to "Well-founded recursion done right" | Herman Geuvers, Gijs Pennings | 15m |
Systematic pattern for well-founded recursion: add an auxiliary accessibility argument so Coq/Rocq accepts definitions as structural, generate the two small… | ||
| Towards a Mechanization of the ECMAScript (JavaScript) Proposal "Temporal" | Aria B. Eide, Vebjørn S. Øiestad, Mikhail Barash | 15m |
Mechanization covers about 43 functions of a 500+ function Temporal proposal (≈200 date/time functions), producing 3,000 lines of Rocq code and proofs; one… | ||
| Formal Assurance for Railway Interlockings: Verifying Z3 SAT Proofs with Tseitin in Rocq | Harry Bryant, Andrew Lawrence, Monika Seisenberger, Anton Setzer | 15m |
Verifies Z3 SAT proof logs by checking RUP format steps and Tseitin transformations inside Rocq, extracting a fully verified proof checker and proving each… | ||
| Specifying and Verifying the NOVA Microhypervisor in Concurrent Separation Logic | Hoang-Hai Dang, Gregory Malecha | 11m |
Verification of the NOVA microhypervisor uses BRiCk C++ program logic built on Iris and Skylabs proof automation to prove concurrency properties of about… | ||
| Abstract VCG: Tie-breaking rules in VCG mechanism design | Zhan JING, Pierre Jouvelot | 14m |
Computer-checked solutions resolve how VCG handles equal bids in sponsored search by parameterizing argmax tie-breaking functions and proving incentive… | ||
| Session with the Rocq Development Team | Matthieu Sozeau, Yann Leray, Gaetan Gilbert | 42m |
Rocq releases 9.0 and 9.1 ship a single rag binary, a split of the standard library into a minimal core plus a separate stdlib, and fixes to the guard checker… | ||
| Trocq parametricity translations for inductives | Tomas Vallejos Parada | 14m |
Claims an extension to the Trocq plugin that automatically generates the lattice of parametricity translations for inductive types with parameters and… | ||
| Formalizing a First-order Differentiable Logic with MathComp | Jairo Miguel Marulanda-Giraldo | 13m |
Claims a formalized, well-behaved first-order differentiable logic built on MathComp by extending its analysis libraries with a correct power function for… | ||
| Implementing parametricity in Rocq-ELPI | Cyril Cohen, Vojtěch Štěpančík | 15m |
Implements a sequent-calculus style binary parametricity as a logic program inside Rocq-ELPI, translating each inference rule to an ELPI clause that produces… | ||
| Lambda JS à la Carte | Kirill Golubev, Mikhail Barash, Jaakko Järvi | 16m |
Presents a modular mechanization of JavaScript semantics using the Coq à la Carte approach to avoid monolithic encodings. It addresses the maintenance and… | ||
| The HOL-Light library of Multivariate real analysis in Rocq | Abdelghani Alidra, Claudio Sacerdoti Coen, Frédéric Blanqui | 15m |
Coq-HOL-Light is a native Rocq library translated from HOL-Light that brings 20,000 theorems in real, complex, vector and algebraic analysis into Rocq via a… | ||
| Scalable Type Inference for Intrinsically-Typed Binders | Max Kurze, Clément Pit-Claudel, Sebastian Ertel | 15m |
Claims that guided type inference using bi-directionality hints plus automation in Ltac2 makes intrinsically-typed binders practical in Rocq: variable contexts… | ||
| Future-Proofing Numerical Accuracy with Formal Specifications | Ariel E. Kellison | 48m |
Argues that making floating‑point assumptions explicit and parameterized preserves accuracy as hardware and formats diversify. Builds LA proof, a library of… | ||
| Verification of Templated Code in C++ | Gregory Malecha, David Swasey, Simon Hudon | 15m |
Claims a method to verify C++ templates without expanding the trusted computing base by treating unresolved symbols as hygienic macros and using a shallowly… | ||
| Nested Inductive Types for Rocq and Lean | Thomas Lamiaux, Yannick Forster, Matthieu Sozeau, Nicolas Tabareau | 21m |
Nested nested inductive types like RoseTree now get a syntactic check that classifies well behaved cases and rejects ones that rely on reduction tricks… | ||
| Enhancing universe polymorphism for Rocq: Algebraic universes, consistency checking(…) | Matthieu Sozeau, Marc Bezem | 16m |
Mechanical refinement of Bezem–Coquand’s decision procedure is implemented and machine-verified inside a Rocq branch, producing a concrete universe model and… | ||
| Crane Lowers Rocq Safely into C++ | Matthew Z. Weaver, Joomy Korkut | 17m |
Crane extracts Rocq into idiomatic, readable C++ that maps Rocq inductive types and monadic effects to either stdlib or Bloomberg core types, generates… | ||
| Recursive Mutexes in Separation Logic | Ke Du, William Mansky, Paolo G. Giarrusso, Gregory Malecha | 15m |
Develops a separation-logic specification for recursive mutex built on the Brick logic and derived from a lower-level logically-atomic spec, with a per-thread… | ||
| nothing matches | ||