3 june 2024, Nantes

• 10h - 10h30 : Welcome
• 10h30 - 10h45 : Opening - Guilhem Jaber
• 10h45 - 12h15 : A detailed introduction of Coq's guard condition - Hugo Herbelin
• 12h15 - 13h30 : Lunch (lunch boxes will be provided)
• 13h30 - 14h15 : Guard condition in MetaCoq - Yannick Forster & Yee-Jian Tan
• 14h15 - 15h : Formalizing proof of strong normalization for MLTT (logrel project) - Meven Bertrand or Kenji Maillard
• 15h - 15h45 : Coffee break
• 15h45 - 16h30 : An introduction to guarded recursive types - Guilhem Jaber
• 16h30 - 17h : Discussion