🐔
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

Agda as a programming language

module Padova2025.ProgrammingBasics where
open import Padova2025.ProgrammingBasics.Booleans
open import Padova2025.ProgrammingBasics.Operators
open import Padova2025.ProgrammingBasics.HigherOrder
open import Padova2025.ProgrammingBasics.Naturals
open import Padova2025.ProgrammingBasics.DependentFunctions
open import Padova2025.ProgrammingBasics.Lists
open import Padova2025.ProgrammingBasics.Vectors