CoqWG 2023‐12‐18
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
https://univ-nantes-fr.zoom.us/j/9539898681
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)
- 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)
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).
- 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
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.
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.