second part of the course teoria dei tipi • begin April 27th, 2023 • 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,
- practically explore type theory
- appreciate mathematics from a new point of view and
- verify the correctness of programs.

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

Thursdays from 4.30 pm till 6.30 pm (Italian time)

Fridays from 2.30pm till 4.30 pm

*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, and basic proofs regarding natural numbers**Sheet 3.**basic proofs with equality**Sheet 4.**equational reasoning, relations**Sheet 5.**correctness of insertion sort**Sheet 6.**ordinal numbers**Sheet 7.**termination and well-founded recursion**Sheet 8.**Cubical Agda

**Transcript of session 1.****Transcript of session 2.****Transcript of session 3.****Transcript of session 4.****Transcript of session 5.****Transcript of session 6.****Transcript of session 7.****Transcript of session 8.****Transcript of session 9.****Transcript of session 10.****Transcript of session 11.****Transcript of session 12.**

**Recordings available here.**

*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.*

**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

**Agda as a proof language**- de Morgan
- relations
- equality type, zero = zero, neg² = id, function extensionality
- lemmas about natural numbers
- general induction

**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*

- 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

phone: +49 176 95110311 (also Telegram)