Rocq'n'share 2026 - rocq-prover/rocq GitHub Wiki

The second Rocq'n'share meeting will take place at EPFL in Lausanne, Switzerland from Monday June 29th to Friday July 3rd 2026.

Rocq'n'share is a meeting place for developers of The Rocq Prover and of its extensions: tactic languages, metaprogramming languages, libraries, plugins, verification frameworks, compilers, decision procedures, etc. The goal of the meeting is to disseminate knowledge on the implementation of Rocq and its extension frameworks, discuss design decisions, improve documentation, and hack together on specific projects.

Useful links

• Main event website
• Registration (free but required!)
• Zulip channel

Talks and tutorials

(Add yourself below if you'd like to propose a talk or tutorial)

• @SkySkimmer "How to solve a Rocq bug"
• Dario Halilovic: "Camltac: OCaml as a Tactic Language"

projects

• port platform docs to alectryon?

Sponsors

This event is financially supported by the Swiss Informatics Foundation — Informatik Stiftung Schweiz.