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)