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

Thursdays and Fridays from 4.30 pm till 6.00 pm (Italian time)

*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

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

Zoom link (experimental), Meeting ID: 654 3564 1178, Passcode: ?#%&9U

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