Agda,
a beautiful proof assistant


second part of the course teoria dei tipi • begin April 11th, 2024 • by Ingo Blechschmidt

Welcome to our joint course on Agda. :-)

Agda is a programming language. But Agda is much more than that: Agda is also a proof language. We can write up mathematical proofs in Agda, even proofs concerning infinite or uncomputable objects. Furthermore, Agda is not static: Agda is also a proof assistant helping us devise proofs. With Agda, we can …:

I hope you will enjoy the course. Questions and suggestions are always welcome!


Schedule

Thursdays and Fridays from 4.30 pm till 6.00 pm (Italian time)


Exercise sheets

Suggested exercises and their solutions will be posted here.

Also see exercises from the previous year.


Transcripts and recordings

Recordings available here. (audio/video will be joined soon) (The recordings from the previous year are already joined.)


Online participation via Zoom

Zoom link (experimental), Meeting ID: 654 3564 1178, Passcode: ?#%&9U


Syllabus

First draft based on earlier Agda workshops. After the basics are cleared, we can explore lots of different tangents. Your input is very much welcome.

  1. Agda as a programming language
  2. Agda as a proof language
  3. Exploring Agda

References


Contact

phone: +49 176 95110311 (also Telegram)