🐔
Let's play Agda Beta

Welcome
Agda as a programming language
Agda as a proof language
1. Predicates on natural numbers
2. Negation
3. Equality
4. Logical connectives
5. Termination and well-founded recursion
Verified algorithms
1. Post-hoc verification
2. Correct by construction
3. Case study: Insertion sort
  1. Implementation
  2. Post-hoc verification
4. Case study: Compiler and interpreter
Cubical Agda
1. Issues with standard Agda
  1. Function extensionality
  2. Quotients
  3. The identity types of the universe
2. A mathematical rosetta stone
3. First steps
Computational content of classical logic
1. Convenient fictions
  1. Minimas
  2. Drinkers
2. Sarcastic interpretation of classical logic
3. Case study: Dickson's lemma

📥 Download raw

Getting Agda

For this tutorial, you do not need to install Agda on your computer. Instead, an online version of Agda is embedded into this website.

For larger experiments, not tied to the exercises of this tutorial, you can use the Agdapad. Again, no installation is required.

For installing Agda on your own computer, check out the official Agda website.