École de Printemps d'Informatique Théorique 2025 - Sciencesconf.org

Week Mon. 19 Tue. 20 Wed. 21 Thu. 22 Fri. 23 List

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

CNRS

CCSD

Sciencesconf