=== Workshop on the guard condition of Coq ===

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