second part of the course teoria dei tipi • begin April 22th, 2022 • 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!*

Zoom:
https://unipd.zoom.us/j/85250849100?pwd=MHo4K0NBb240SjlUWG42ME44bkRLdz09

Meeting ID: 852 5084 9100

Passcode: 123456

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.**functions with vectors and lists**Sheet 3.**first steps in proving properties of natural numbers**Sheet 4.**equality of functions, numbers, lists and vectors**Sheet 5.**equational reasoning, relations**Sheet 6.**correctness of insertion sort**Sheet 9.**sets as trees**Sheet 10.**termination and well-founded recursion

**Transcript of session 1.**Booleans, natural numbers, basic functions**Transcript of session 2.**Partial solutions to exercise sheet 1, vectors, basic functions with vectors**Transcript of session 3.**First steps in proving: even and odd numbers**Transcript of session 4.**First steps in proving: equality of natural numbers**Transcript of session 5.**More on equality of natural numbers; also polymorphic equality**Transcript of session 7.**Correctness of insertion sort**Transcript of session 9.**Sets as trees: introduction to one of the most important models of CZF and to the connection between set theory and type theory**Transcript of session 10.**On termination and well-founded recursion**Transcript of session 11.**Function extensionality, quotients, setoids**Transcript of session 12.**Cubical type theory**Transcript of session 13.**Extracting constructive content from classical proofs (illustrated with Dickson's lemma)

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

mail: iblech@speicherleck.de

phone: +49 176 95110311 (also Telegram)