IRIF - Université Paris Cité, Bâtiment Sophie Germain, salle 3052 and 3063
The meeting will be held in hybrid mode, i.e., both via Zoom and in the form of in-person meetings at IRIF (Salle 3052 and 3063).
Please note: the first afternoon session will take place in Salle 3063, while all other sessions will take place in the main seminar room on the third floor of IRIF (Salle 3052).
| Time | Speaker | Title | |
|---|---|---|---|
| 10:00 - 10:05 | Kazuhiko Sakaguchi | Introduction of the IC Rocq workgroup | |
| 10:05 - 10:30 | Samuel Arsac | Adhesive Category Theory for Graph Rewriting in Rocq | |
| 10:30 - 10:45 | Samuel Arsac | On Computable (Co-) Equalizers | |
| 10:45 - 11:30 | Manuel Catz | Diagrammatic (Proofs in) Rocq | |
| 12:00 - 12:30 | Kazuhiko Sakaguchi | Tactics Modulo Associativity and Cancellation for Category Theory | |
| 12:30 - 13:00 | Nicolas Behr | Conditional Hyperdoctrines - An Update | |
| 14:00 - 15:00 | discussion on proof data management/UI design/CoREACT wiki | ||
| 15:30 - 17:00 | discussion on formalization/implementation of Instantiation Calculus in Rocq | ||