CoqWG 2023‐12‐18 - coq/coq GitHub Wiki
Organization
The next Coq Working Group will take place on December, 18th 2023 in LS2N, Nantes (Google Maps), building 34.
Organizers : Pierre-Marie Pédrot, Nicolas Tabareau
Online access
https://univ-nantes-fr.zoom.us/j/9539898681
Topics
Please add your topic, and an estimated duration.
The morning session will be broadcast, topics relevant to the whole Coq community should go there.
- 10:00-10:15: Strengthening the social contract for Coq's CI (15 min - Karl, followup to a topic discussed in this call)
- 10:15-10:30: State of the roadmap (15 min - Karl, possibly leading up to Coq 9.0 topic below)
- 10:30-11:30: Let's be brave and talk about Coq 9.0 (1h - Enrico)
- 11:30-12:00: coq-lsp update (30+15 Emilio, I can be flexible with time)
The afternoon session will be split in topic groups and likely not broadcast.
- Some investigations with the guard condition (10 mins + discussions - Hugo)
- Towards a direct implementation of namespaces? (10 mins + possible discussions - Hugo)
Schedule
- 9:30-10:00: welcome coffee
- 10:00-12:00: morning session (plenary session)
- 12:00-14:00: lunch (see below)
- 14:00-18:00: afternoon session (topic groups)
- 20:00: dinner (see below)
Lunch and Dinner Events
Dinner will take place at Balthazar.
IMPORTANT: Both lunch and dinner are free, but you must be registered for organisation purposes. If you plan on only attending one (or none) of the meals, please indicate so in the list below with the following code: N (neither lunch nor dinner), L (lunch only), D (dinner only).
Participants (please register yourself)
- Enzo Crance L
- Emilio J. Gallego Arias
- Gaëtan Gilbert
- Hugo Herbelin
- Assia Mahboubi
- Karl Palmskog
- Pierre-Marie Pédrot
- Nicolas Tabareau
- Théo Winterhalter
- Enrico Tassi
- Meven Lennon-Bertrand
- Yann Leray
- Kazuhiko Sakaguchi
- Tomas Diaz
- Mara Malewski
- Matthieu Sozeau
- Ambrus Kaposi D
- Cyril Cohen
- Yannick Forster
- Rafaël Bocquet L
- Théo Zimmermann L
Related events
The 18th-22nd week will be an eventful one at Gallinette. You may consider extending your stay.
- On Tuesday 19th 10AM, amphitheater B, ground floor of 34 building, Enzo Crance will defend his PhD, Meta-programming for Proof Transfer in Dependent Type Theory .
- On Wednesday 20th, we will have a day-long workshop involving a subset of the members of the PhD juries above and below.
- On Thursday 21st, 2pm, amphitheater B, ground floor of 34 building, Martin Baillon will defend his PhD, Continuity in Type Theory.