A List of Tutorials

Note

Some of the materials linked on this page have been created for older versions of Agda and might no longer apply directly to the latest release.

Books on Agda

• Phil Wadler, Wen Kokke, and Jeremy G. Siek (2019). Programming Languages Foundations in Agda

• Aaron Stump (2016). Verified Functional Programming in Agda

Tutorials and lecture notes

• Jesper Cockx (2021). Programming and Proving in Agda. An introduction to Agda for a general audience of functional programmers. It starts from basic knowledge of Haskell and builds up to using equational reasoning to formally prove correctness of functional programs.

• Musa Al-hassy (2019). A slow-paced introduction to reflection in Agda.

• Jesper Cockx (2019). Formalize all the things (in Agda).

• Jan Malakhovski (2013). Brutal [Meta]Introduction to Dependent Types in Agda.

• Diviánszky Péter (2012). Agda Tutorial.

• Ana Bove, Peter Dybjer, and Ulf Norell (2009). A Brief Overview of Agda - A Functional Language with Dependent Types (in TPHOLs 2009) with an example of reflection. Code.

• Andreas Abel (2009). An Introduction to Dependent Types and Agda. Lecture notes used in teaching functional programming: basic introduction to Agda, Curry-Howard, equality, and verification of optimizations like fusion.

• Ulf Norell and James Chapman (2008). Dependently Typed Programming in Agda. This is aimed at functional programmers.

• Ana Bove and Peter Dybjer (2008). Dependent Types at Work. A gentle introduction including logic and proofs of programs.

• Anton Setzer (2008). Lecture notes on Interactive Theorem Proving. Swansea University. These lecture notes are based on Agda and contain an introduction of Agda for students with a very basic background in logic and functional programming.

Videos on Agda

• Conor McBride (2014). Introduction to Dependently Typed Programming using Agda. (videos of lectures). Associated source files, with exercises.

• Daniel Licata (2013). Dependently Typed Programming in Agda (at OPLSS 2013).

• Daniel Peebles (2011). Introduction to Agda. Video of talk from the January 2011 Boston Haskell session at MIT.

Courses using Agda

• Computer Aided Reasoning Material for a 3rd / 4th year course (g53cfr, g54 cfr) at the university of Nottingham 2010 by Thorsten Altenkirch

• Type Theory in Rosario Material for an Agda course in Rosario, Argentina in 2011 by Thorsten Altenkirch

• Software System Design and Implementation, undergrad(?) course at the University of New South Wales by Manuel Chakravarty.

• Tüübiteooria / Type Theory, graduate course at the University of Tartu by Varmo Vene and James Chapman.

• Advanced Topics in Programming Languages: Dependent Type Systems, course at the University of Pennsylvania by Stephanie Weirich.

• Categorical Logic, course at the University of Cambridge by Samuel Staton.

• Dependently typed functional languages, master level course at EAFIT University by Andrés Sicard-Ramírez.

• Introduction to Dependently Typed Programming using Agda, research level course at the University of Edinburgh by Conor McBride.

• Agda, introductory course for master students at ELTE Eötvös Collegium in Budapest by Péter Diviánszky and Ambrus Kaposi.

• Types for Programs and Proofs, course at Chalmers University of Technology.

• Advanced Functional Programming (in German), course at Ludwig-Maximilians-University Munich.

• Dependently typed metaprogramming (in Agda), Summer (2013) course at the University of Cambridge by Conor McBride.

• Computer-Checked Programs and Proofs (COMP 360-1), Dan Licata, Wesleyan, Fall 2013.

• Advanced Functional Programming Fall 2013 (CS410), Conor McBride, Strathclyde, notes from 2015, videos from 2017.

• Interactive Theorem proving (CS__336), Anton Setzer, Swansea University, Lent 2008.

• Inductive and inductive-recursive definitions in Intuitionistic Type Theory, lectures by Peter Dybjer at the Oregon Programming Languages Summer School 2015.

• Introduction to Univalent Foundations of Mathematics with Agda , MGS 2019 Martín Hötzel Escardó

• Higher-Dimensional Type Theory (CSCI 8980), courses on homotopy type theory and cubical type theory, Favonia, the University of Minnesota, Spring 2020

• Correct-by-construction Programming in Agda, a course at the EUTYPES Summer School ‘19 in Ohrid.

• Lectures on Agda, a course by Peter Selinger at Dalhousie University, Winter 2021.

Miscellaneous

• Agda has a Wikipedia page)