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

module Padova2025.VerifiedAlgorithms.InsertionSort where

Case study: Insertion sort

open import Padova2025.VerifiedAlgorithms.InsertionSort.Implementation
open import Padova2025.VerifiedAlgorithms.InsertionSort.PostHoc