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