Coq Users and Developers Workshop 2024
Eigth Coq Users and Developers Workshop, July 1st - July 5th, 2024, Nantes Université (Nantes, France)
This page collects useful info for the participants in the 8th Coq Users and Developers Workshop.
The Coq Users and Developers Workshop is an event that brings together the core developers of Coq and people interested in understanding, improving or extending the system.
All Coq related projects are welcome.
More information can be found on the wiki or asked on the Zulip channel: https://coq.zulipchat.com/#narrow/stream/433315-CUDW-2024
The event will be in person only, no remote attending.
We want the event to be safe to attend. We will enforce the Coq code of conduct
IMPORTANT: The CUDW is free, but for organization purposes please register yourself in alphabetical order in the list below, with intended arrival and departure dates.
The Workshop takes place at the LS2N in Nantes, from Monday July, 1st to Friday, July 5th. Travel and accommodation hints here or here (pages from other events organized in the same place).
The schedule will run from Monday afternoon (1pm) to Friday after lunch (~ 2pm). The room is available the entire week (arriving early/leaving late is possible).
For any question please contact Pierre-Marie Pédrot by e-mail or (faster) on the Coq Zulip.
IMPORTANT: The CUDW is free, but for organization purposes please register yourself in alphabetical order in the list below, with intended arrival and departure dates.
- Gaëtan Gilbert (full week)
- Hugo Herbelin (full week)
- Janno [Jan-Oliver Kaiser] (full week)
- Thomas Lamiaux (full week)
- Yann Leray (full week)
- Assia Mahboubi (full week)
- Pierre-Marie Pédrot (full week)
- Pierre Roux (full week)
- Nicolas Tabareau (full week)
- Enrico Tassi (full week)
- Kazuhiko Sakaguchi (full week)
If there is a specific topic you would like to work on, or discuss about with the core devs, we recommend that you write it down here as well. This will allow to elaborate a schedule so that people can work in parallel groups, and synchronize regularly.
- (Janno) Primitive projections, specifically removing compatibility constants. It seems like we cannot get the behavior of the kernel right as long as they still exist (https://github.com/coq/coq/issues/18977)
- (Janno) Reviving https://github.com/coq/coq/pull/17839 with new
Constrconstructors instead of (ab)using primitives - (Thomas Lamiaux) Tutorials for Ltac2
- (Nicolas) implementation of a sort and universe polymorphic standard library
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.