Agda
💻 Agdapad for running Agda in the browser
👨‍🏫 Notes for a 2024 tutorial on Agda (including exercises and recordings)

Code presented in the talk
👷 Insertion sort
♾️ Dickson's lemma

Proofs as programs
💥 Curry–Howard correspondence
🔥 Propositions as types
⚙️ Notes for a 2024 course on the computational content of classical proofs

Alternatives to Agda
🐓 Rocq (née Coq) and Lean:
   - based on dependent type theory, like Agda
   - proofs are typically written in imperative "proof script" style
     instead of Agda's functional "proof term" style
   - Lean: community centered around classical mathematics
   - Rocq: industrial-strength
🟨 Isabelle:
   - based on higher-order logic
   - proof scripts instead of proof terms
   - famous for large library of 20th century analysis
👩‍🏫 Many others! Seminar Every proof assistant run by Andrej Bauer

Contact
👤 Ingo Blechschmidt
💬 +49 176 95110311 (Signal, Telegram, SMS)