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 …:

• develop proofs and ensure their correctness,
• verify the correctness of programs,
• practically explore type theory,
• appreciate mathematics from a new point of view and
• unlock new ways of mathematical collaboration.

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.

• Sheet 1. basic functions with booleans and natural numbers
• Sheet 2. basic functions with lists and vectors, some proofs about natural numbers and lists
• Sheet 3. proofs concerning equality
• Sheet 4. correctness of algorithms
• Sheet 5. termination
• Sheet 6. cubical Agda

Also see exercises from the previous year.

Transcripts and recordings

• Transcript of session 1. first steps
• Transcript of session 2. second steps
• Transcript of session 3. relations on natural numbers
• Transcript of session 4. equality
• Transcript of session 5. equational reasoning, correctness of algorithms
• Transcript of session 6. correctness of insertion sort
• Transcript of session 7. termination
• Transcript of session 8. interpreter and compiler for a toy programming language
• Transcript of session 9. cubical Agda
• Transcript of session 10, part one. game theory
• Transcript of session 10, part two. simply-typed lambda calculus
• Transcript of session 11, part one. mutable state
• Transcript of session 11, part two. Peano Arithmetic
• Transcript of session 12. Sarcastic interpretation of classical logic
• Transcript of session 13. Graphs and graph algorithms

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
   • Bool, id, neg, ¬_, and
   • Nat, add2, pred, recursion
   • "types are first-class", "everything has a type"
   • Weird
   • NatList
   • List
   • Vector
2. Agda as a proof language
   • de Morgan
   • relations
   • equality type, zero = zero, neg² = id, function extensionality
   • lemmas about natural numbers
   • general induction
3. Exploring Agda
   • certified sorting
   • sets as trees, Russell's paradox
   • simply typed lambda calculus
   • minima of sets of natural numbers, Higman's Lemma
   • setoids
   • cubical Agda
   • your suggestion here

References

• Programming Language Foundations in Agda (by Wadler, Kokke and Siek)
• Programming and Proving in Agda (by Cockx)
• Introduction to Univalent Foundations of Mathematics with Agda (by Escardó)
• Dependent Types at Work (by Bove and Dybjer)
• More on correct by construction (by Cockx)
• More on the double-negation translation

Contact

phone: +49 176 95110311 (also Telegram)