Rocq'n'code 2025 - rocq-prover/rocq GitHub Wiki

The First Rocq'n'code meeting (previously known as Coq Users and Developers Workshop) will take place at Inria Paris from Monday June 23rd (or 24th) to the 27th.

Rocq'n'code is a meeting place for developers of the Rocq Prover and of its extensions: libraries, plugins, verification frameworks, compilers, decision procedures... The program will be a mix of scientific/technical talks and small group design/programming sessions.

Rooms

  • Monday/Tuesday: Emmy Noether
  • Wednesday/Thursday: Gilles Kahn + Sally Floyd
  • Friday: Anita Borg

Talk proposals

Add talk proposals here, they will be scheduled during the week (30min or 1h slots)

  • A new, correct and complete algorithm for cumulativity checking with algebraic universes (Matthieu Sozeau) (30min).
  • A new core library based on universe & sort polymorphism (Josselin Poiret, Matthieu Sozeau, Nicolas Tabareau, ...) (1h)
  • 'Erased': a new sort for proof-relevant but computationally-irrelevant data (Johann Rosain, Matthieu Sozeau, Théo Winterhalter) (30min).
  • TBA, several ideas depending on interest (interfaces, ML APIs, etc...) (Emilio, 30-60 min)
  • Rocq state system explanation (summary, libobject, proof state, etc) (Gaëtan, IDK)
  • HConstr: context-aware hashconsing (Gaëtan, 30min or possibly less?)
  • ...

Project proposals

Add project proposals here, to be scheduled during the week. We'll gather small groups working on each of these.

  • Use proper identifiers rather than 0...100 for notation levels (Pierre Roux)

  • port equations tactics from ltac1 to ltac2

  • port ring tactic from ltac1 to ltac2

  • ...

  • Emilio:

    • Dune projects
    • coq-lsp projects
    • jsCoq projects
    • petanque projects
    • Rocq projects

Attendees (Mandatory to get in!)

  • Matthieu Sozeau