Monday, May 19, 2025
Time | Event | (+) |
08:45 - 09:00 | Welcome - Denis Kuperberg, Guilhem Jaber, Luigi Santocanale & Alexis Saurin | |
09:00 - 10:30 | Back to basics - D Kuperberg, L Santocanale, A Saurin | |
10:30 - 10:50 | Coffee break | |
10:50 - 12:20 | Basics of category theory, algebras and coalgebras - F Jafarrahmani & D Petrisan | |
12:20 - 14:00 | Lunch | |
14:00 - 15:15 | The μ-calculus and its proof-theory - Bahareh Afshari | |
15:15 - 16:15 | Automata on infinite structures - Karoliina Lehtinen | |
16:15 - 16:45 | Coffee break | |
16:45 - 18:15 | Bisimulation and coinductive types in the Rocq proof assistant - Damien Pous & Yannick Zakowski | |
19:30 - 20:45 | Dinner |
Tuesday, May 20, 2025
Time | Event | (+) |
08:50 - 10:30 | Basics of category theory, algebras and coalgebras - Farzad Jafarrahmani & Daniela Petrisan | |
10:30 - 10:50 | Coffee break | |
10:50 - 12:20 | The μ-calculus and its proof-theory - Bahareh Ashari | |
12:20 - 14:00 | Lunch | |
14:00 - 15:00 | Automata on infinite structures - Karoliina Lehtinen | |
15:00 - 16:15 | Bisimulation and coinductive types in the Rocq proof assistant - Damien Pous & Yannick Zakowski | |
16:15 - 16:45 | Coffee break | |
16:45 - 18:00 | Higher-order languages, Categories and Automata - Paul-André Melliès & Daniela Petrisan | |
19:30 - 20:45 | Dinner |
Wednesday, May 21, 2025
Time | Event | (+) |
08:50 - 10:30 | Software Verification via Fixed-Point Logics: Constraint Solving, Cyclic-Proof Search, and Strategy Synthesis - Hiroshi Unno | |
10:30 - 10:50 | Coffee break | |
10:50 - 12:20 | Higher-order languages, Categories and Automata - Paul-André Mellies & Daniela Petrisan | |
12:20 - 13:30 | Lunch | |
13:30 - 18:00 | Free afternoon - Organized hike or free afternoon | |
19:30 - 21:00 | Banquet | |
21:00 - 23:00 | Cocktail |
Thursday, May 22, 2025
Time | Event | (+) |
08:50 - 11:00 | Guarded recursive types - Daniel Gratzer & Adrien Guatto | |
11:00 - 11:20 | Coffee break | |
11:20 - 12:20 | Software Verification via Fixed-Point Logics: Constraint Solving, Cyclic-Proof Search, and Strategy Synthesis - Hiroshi Unno | |
12:20 - 14:00 | Lunch | |
14:00 - 15:15 | Bisimulation and coinductive types in the Rocq proof assistant - Damien Pous & Yannick Zakowski | |
15:15 - 16:15 | Circular and non wellfounded proofs: expressiveness and semantics - Anupam Das & Farzad Jafarrahmani | |
16:15 - 16:45 | Coffee break | |
16:45 - 18:15 | Circular and non wellfounded proofs: expressiveness and semantics - Anupam Das & Farzad Jafarrahmani | |
19:30 - 20:45 | Dinner |
Friday, May 23, 2025
Time | Event | (+) |
08:50 - 10:50 | Guarded recursive types - Daniel Gratzer & Adrien Guatto | |
10:50 - 11:20 | Coffee break | |
11:20 - 12:20 | Conclusion and Open Problems | |
12:20 - 14:00 | Lunch | |
14:00 - 17:00 | Free Discussions |