Program

Monday May 25

  • 12:00 welcome Lunch
  • 14:00 – 15:30 / 16:00 – 17:30: Introduction to Homotopy Type Theory (Andrej Bauer)
  • Evening: Tools install Party (Coq, Agda, Cubical Agda, other)

Tuesday May 26

  • 9:00 – 10:30 / 11:00 – 12:30: The Coq-HoTT library (Bas Spitters)
  • 14:30 – 16:00: Hands-on Session (Coq-HoTT)
  • 16:30 – 18:00: The Arend Proof Assistant (Valery Isaev)

Wednesday May 27

  • 9:00 – 10:30 / 11:00 – 12:30: Models of (Univalent) Type Theory (Andy Pitts)
  • 14:00 – 18:00: Excursion
  • 18:30: Poster Session

Thursday May 28

  • 9:00 – 10:30 / 11:00 – 12:30: Cubical Type Theory (Anders Mörtberg)
  • 14:30 – 16:00: Hands-on Session (Cubical Agda)
  • 16:30 – 18:00: Directed Homotopy Type Theory (Paige North)

Friday May 29

  • 9:00 – 10:30 / 11:00 – 12:30: Synthetic Homotopy Theory (Guillaume Brunerie)
  • 12:30 – 13:00: Wrap up / Closing of the School

Comments are closed.