Agda in Padova 2025

📝 Transcripts
Session 1. Bool, ℕ, List, pattern matching, implicit parameters
Session 2. Even, Odd, equality
Session 3. Equational reasoning
Session 4. Logical connectives
Session 5. Computational content of classical logic, ordinal numbers
Session 6. More on ordinal numbers, topos theory
Session 7. Program verification, sets as trees
Session 8. Limitations, axiom of choice
Session 9. Cubical Agda
Session 10. Toy programming language, Peano arithmetic, forcing

🎞 Recordings
Here

❤️ Recommended exercises
Location of exercises: Let's play Agda
Week 1. Up to but excluding "Logical connectives"
Week 2. Up to and including "Well-founded recursion"
Week 3. All exercises are possible, in particular "Numbers larger than infinity" and "Computational content of classical mathematics"
Week 4. All exercises, in particular "Verified algorithms" and "Issues with standard Agda"
Week 5. All exercises, in particular "Cubical Agda"

🌐 Links
Midlands Graduate School
Alternatives to Agda

💥 Upcoming conferences
CIRM: Synthetic mathematics, logic-affine computation and efficient proof systems
Autumn school: Proof and Computation

💬 Contact
+49 176 95110311 (Signal, Telegram, SMS)