Are you itching to learn more about the internals of your favorite proof assistant? Do you have a feature to advocate for? Do you need help implementing an extension or hacking the kernel? Do you feel ready to step up and fix that bug that’s been pestering you for years?
Join us for Rocq'n'Share 2026, held from June 29th to July 3rd on EPFL’s main campus in Lausanne!
Participants
Alexandre PinazzaEPFL SYSTEMF/VCA
Andrei Duma
Cécile MarconINRIA Lyon
Clément Pit-ClaudelEPFL SYSTEMF
Cyril CohenInria
Dario HalilovicEPFL SYSTEMF
Éric TanterUniversity of Chile & Inria
Gabriel SchererINRIA Paris
Gaëtan GilbertInria
Hugo HerbelinIRIF - Inria
Iulia Dumitru
JannoSkyLabs AI
Jérémy ThibaultEPFL SYSTEMF
Johannes HostertETH Zurich
Kacper KorbanEPFL SYSTEMF
Marcin WojnarowskiEPFL SYSTEMF
Matteo CalosciUniversità di Firenze
Matthieu SozeauInria Paris
Miriam PolzerGoogle
Nate FosterEPFL and Jane Street
Nicolas TabareauInria
Peio BorthelleINRIA, ENS de Lyon
Pierre-Marie PédrotINRIA
Ralf JungETH Zurich
Rodolphe LepigreSkyLabs AI
Rudy PetersonEPFL SYSTEMF
Samy AvrillonENS de Lyon
Sylvain BorgognoInria
Théo ZimmermannTélécom Paris
Tony LawCentraleSupélec
Victor DengEPFL SYSTEMF
Wassim Ait MoussaInria
Yann LerayInria Gallinette, Nantes
Yawen GuanEPFL SYSTEMF
Format
Rocq'n'Share is a meeting place for developers and power users of The Rocq Prover and of its extensions: tactic languages, metaprogramming languages, libraries, plugins, verification frameworks, compilers, decision procedures…
The week will be organized around short presentations and brainstorming sessions in the mornings, and focused discussion and implementation sessions in the afternoons. Rocq developers will bring good starting projects for beginners, or you can bring your own ideas and work-in-progress implementation to receive expert support!
Any hotel on campus, in Lausanne, or in Morges (cheaper and somewhat closer to EPFL) should work.
Travel
To Switzerland
Take a flight or train to Geneva (1h away) or Zurich (2.5h away), or a train to Lausanne (0.5h away). (There will be some disruptions on the Geneva–Lausanne line in the night of 27–28 June.)
To EPFL
Use public transport from your accommodation: choose among bus 1 from Lausanne (get off at Ecublens VD, EPFL/Colladon), bus 701 from Morges (get off at St-Sulpice VD, Parc Scientifique), and metro 1 from Renens or Lausanne (get off at Ecublens VD, EPFL). These trips will most likely be covered by the transport pass provided by your hotel.
Public transport
Vaud (our canton) is organized into 188 Mobilis zones. Lausanne is in zone 11; EPFL is in zone 12; Morges is in zones 30 and 33.
Staying at a Lausanne or Morges-area hotel entitles you to some free or discounted public transportation:
Lausanne hotels provide a public-transport pass with broad enough coverage (zones 11/12) to travel between Lausanne and EPFL. Your hotel will not hand it to you until you check in, but the ride from the Lausanne train station to your hotel or to EPFL on the same day is still covered (just show your hotel reservation).
Morges hotels provide the Slow pass, which includes a 20 CHF voucher per night of stay. This voucher must be redeemed on the MBC website (not the SBB app!). We recommend that you use it to purchase a daily Morges-Lausanne travel card (zones 11/12/30/33), which covers trips to EPFL and to Lausanne throughout the day.
Other visitors can buy tickets or use EasyRide on the SBB/CFF mobile app. Tickets must be purchased before entering public transport.
Rocq setup
# Create an opam switch
opam switch create rocq-dev --packages="ocaml-variants.4.14.2+options,ocaml-option-flambda"
eval $(opam env --switch=rocq-dev --set-switch)
# Rocq
git clone https://github.com/rocq-prover/rocq.git
cd rocq
opam install ./rocq-runtime.opam ./rocq-core.opam
cd ..
# Stdlib
git clone https://github.com/rocq-prover/stdlib.git
cd stdlib
make
cd ..
# VsRocq language server
git clone https://github.com/rocq-prover/vsrocq.git
cd vsrocq/language-server
opam install ./vsrocq-language-server.opam
# then set "vsrocq.path" to the printed vsrocqtop path in your editor settings
Participant-selected topics, in small focus groups.
Friday AM (–): debrief!
Demos, small-group reports, and follow-up plans.
Social events
Weather permitting, we will organize the following events:
Sat drinks
Trade Rocq development stories (and complaints about the weather) over beer at EPFL's premier student pub, Satellite.
Lakeside stroll and beach picnic
Pack a water bottle, a hat, good shoes… and a swimsuit! We will leave EPFL around 17:45 and walk along the lake edge from EPFL to Lausanne, passing by Lausanne sur Mer on the way and stopping in Vidy for dinner.
Note: Our campus is accessible, as are all the rooms used for Rocq'n'Share. If taking public transport, we recommend metro 1 or bus 1. Use the “Reduced mobility” section of EPFL's interactive map to plan your route.
Directions from the “Parc Scientifique” bus 701 stop
Get off the 701 bus at “St Sulpice VD, Parc Scientifique”, turn right (west), and walk towards the stairs.Descend the stairs and turn right (north) to cross through the underpass.Turn left (west) out of the underpassWalk back up the stairs and the dirt trailTurn right (north) towards the campus.Walk one minute between the fancy innovation park buildings and the soon-to-be fancy physics building (currently a construction site).Be careful when crossing the road!Turn left (west) immediately after crossing the road and walk 50 meters along the light brown building.Notice the big recessed door to your right (north). If you reach the déchetterie, you've gone too far!This is it! You will soon enter EPFL.Enter the building. Welcome to EPFL! Take an immediate left…… then an immediate right…… and on to the staircase!Pause to admire the staircase. Its spiraling design is a tribute to the Scala logo, itself also a red spiral. (Some say it's the other way around. Don't believe them.) Time to go up… (The elevator is next to the stairs if you prefer that.)… and up…… and up (enjoy the inspirational quotes on the way!)…… and up…… all the way to the top! Turn left (north) towards the glass wall.The BC 410 sign shows the way: walk all the way to the glass wall.The room's entrance is to the left!You have arrived! Welcome to Rocq'n'share!
Directions from the “EPFL” metro 1 stop
Get off the metro at “Ecublens VD, EPFL”, and turn left (west). Walk down the stairs.Take a left (south) towards the underpass.Walk under the metro, enjoying the inspiring quotes and rainbow colors along the way.Walk up the stairs.Walk south all the way (about two minutes).Slight right at the diagonale.Walk down the diagonale (about one minute).You're in safe territory now, as you have reached the CS faculty buildings. Enter the INM building.Walk through the INM building, keeping to the right.Push the door on your right and go through the corridor to the INN building.Turn left and walk all the way down the INN building.Phew! The BC building. Cross the threshold and notice the staircase.Pause to admire the staircase. Its spiraling design is a tribute to the Scala logo, itself also a red spiral. (Some say it's the other way around. Don't believe them.) Time to go up… (The elevator is next to the stairs if you prefer that.)… and up (enjoy the inspirational quotes on the way!)…… and up…… all the way to the top! Turn left (north) towards the glass wall.The BC 410 sign shows the way: walk all the way to the glass wall.The room's entrance is to the left!You have arrived! Welcome to Rocq'n'share!
Directions from the “EPFL/Colladon” bus 1 stop
Get off bus 1 and walk right (west) until the intersection. Cross the street to the right (north). Be careful when crossing the road!Turn left (west) immediately after crossing the road and
walk 50 meters along the light brown building.Notice the big recessed door to your right (north). If you
reach the déchetterie, you've gone too far!This is it! You will soon enter EPFL.Enter the building. Welcome to EPFL! Take an immediate
left…… then an immediate right…… and on to the staircase!Pause to admire the staircase. Its spiraling design is a
tribute to the Scala logo, itself also a red spiral. (Some say it's the
other way around. Don't believe them.) Time to go up… (The elevator
is next to the stairs if you prefer that.)… and up…… and up (enjoy the inspirational quotes on the
way!)…… and up…… all the way to the top! Turn left (north) towards the
glass wall.The BC 410 sign shows the way: walk all the way to the glass
wall.The room's entrance is to the left!You have arrived! Welcome to Rocq'n'share!
