Coq Andes Summer School (Jan 2020, Chile)

Coq Andes Summer School
January 6-10, 2020
Cajón del Maipo, Chile

The Coq Andes Summer School (CASS) 2020 is a one-week immersive summer school on type theory in general, and on the Coq proof assistant in particular.

CASS is open to advanced and motivated undergraduate and postgraduate students, as well as young academics and professionals. We welcome applications from all over the world. Lectures will be in English.

Registration, shared housing and food are all covered by our projects and sponsors. We also have limited funding to help selected participants traveling from abroad and from outside of the central region of Chile.

Application deadline: October 20, 2019 (AoE)
Check out details and apply:


  • Assia Mahboubi (Inria, FR): Introduction to Coq & SSReflect
  • Matthieu Sozeau (Inria, FR): Programming with dependent types
  • Beta Ziliani (U. Córdoba, AR): Tactic languages
  • Nicolas Tabareau (Inria, FR): Homotopy type theory
  • Alexandre Miquel (U. La República, UR): Realizability
  • Pierre-Marie Pédrot (Inria, FR): Exceptional type theory
  • Guillaume Munch-Maccagnoni (Inria, FR): Call-by-push-value


  • Nicolas Tabareau (Inria, FR)
  • Éric Tanter (U. Chile, CL)

Funded by

  • Projects: ERC CoqHoTT, CONICYT Redes CSEC, Inria Équipe Associée GECO
  • Sponsors: NIC Chile, Inria Chile