🐔
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

References

Programming Language Foundations in Agda – by Philip Wadler, Wen Kokke and Jeremy Siek
Programming and Proving in Agda – by Jesper Cockx
Introduction to Univalent Foundations of Mathematics with Agda – by Martín Escardó
Dependent Types at Work – by Ana Bove and Peter Dybjer
Learn you an Agda – by Liam O’Connor-Davis with additions by William DeMeo
Correct-by-construction programming in Agda – by Jesper Cockx
More on the double-negation translation