Agda in Padova 2026

📋 Questionnaire
I would appreciate if you could fill out this questionnaire.

📝 Transcripts
Session 0. Introduction, ℕ, Bool.
Session 1. Pattern matching, higher-order functions, decision functions,
           implicit parameters, propositions as types, Socrates, Even/Odd.
Session 2. Vectors, equality.
Session 3. Equational reasoning, negation.
Session 4. Logical connectives, termination, program verification.
Session 5. More on program verification, ordinal numbers beyond infinity.
Session 6. Strong induction, toy programming language.
Session 7. Extracting constructive content from classical proofs, limitations of Agda.
Session 8. Quotients, cubical Agda.
Session 9. Impossible programs, infinite-time Turing machines,
           infinite hat problem, sets as trees.

🎞 Recordings
Here

❤️ Recommended exercises
Let's play Agda

🌐 Links
Alternatives to Agda
Stanford Encyclopedia of Philosophy and Logic
Resources of the 2025 course
Andrej Bauer: Five stages of accepting constructive mathematics
Slides on the axiom of choice
Slides on infinite-time Turing machines
Course on constructive mathematics, realizability and double negation (with recordings)
Mathstodon: Andrej Bauer, Martín Escardó

💥 Upcoming events and conferences
7th Workshop on Formal Topology (mid April)
Midlands Graduate School 2026 (mid April)
Colloquia Patavina (on May 5th)
Proof and Computation 2026 (mid September)
Lean for the curious mathematician (mid September)

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