IRIF - Université Paris Cité, Bâtiment Sophie Germain, salle 3052 and 3063
The meeting will be held via Zoom.
| 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 | ||