# 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.

## Miscellaneous¶

- Agda has a Wikipedia page