The repository for this tutorial course is: https://github.com/umazalakain/agda-bcam. You can find the Agda source code in browsable HTML here. The slides for the talk can be found here.

Programming with evidence

• Agda is a programming language and proof assistant
• Mainly developed in Chalmers, Sweden
• Advanced type theoretical prototype language
• Mostly used in
  • Programming Language Theory
  • Category Theory
  • Homotopy Theory
• About me: Uma Zalakain (https://umazalakain.info)

Timetable

• Tutorials:

  • Mon 15:00 - 17:30 (with ~15 minute break)
  • Tue 15:00 - 16:30 (!)
  • Wed 15:00 - 17:30 (with ~15 minute break)
  • Thu 15:00 - 17:30 (with ~15 minute break)
  • Fri: it depends

• Talk (propaganda):

  • Tue 16:30 - 17:30

Resources

• List of tutorials
• Installing Agda