Tutorials

Introductions to Agda:

• Ulf Norell and James Chapman. Dependently Typed Programming in Agda. This is aimed at functional programmers.
• Ana Bove and Peter Dybjer. Dependent Types at Work. A gentle introduction including logic and proofs of programs.
• Ana Bove, Peter Dybjer, and Ulf Norell. A Brief Overview of Agda - A Functional Language with Dependent Types (in TPHOLs 2009) with an example of reflection. Code
• Yoshiki Kinoshita. On the Agda Language (in Japanese) Slides (English) Slides (Japanese)
• Anton Setzer. 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.
• Daniel Peebles. Introduction to Agda. Video of talk from the January 2011 Boston Haskell session at MIT.
• Conor McBride, Introduction to Dependently Typed Programming using Agda (videos of lectures). Associated source files, with exercises.
• Andreas Abel, Agda lecture notes. Lecture notes used in teaching functional programming: basic introduction to Agda, Curry-Howard, equality, and verification of optimizations like fusion.
• Jan Malakhovski, Brutal [Meta]Introduction to Dependent Types in Agda
• Thorsten Altenkirch, Computer Aided Formal Reasoning - online lecture notes
• Daniel Licata. Dependently Typed Programming in Agda (OPLSS 2013).
• Tesla Ice Zhang Some books about Formal Verification in Agda (in Chinese)

General introductions to programming with dependent types:

• Nicolas Oury and Wouter Swierstra. The Power Of Pi (ICFP 2008).
• Conor McBride. Epigram: Practical Programming with Dependent Types (also available from Conor's web page). Lecture notes for the AFP Summer School 2004.