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