Documentation

Release Notes

(There are also tutorials below, under ‘Introductions to Agda’.)

Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology, 2007.
Bengt Nordström, Kent Petterson, Jan Smith. Programming in Martin-Löf’s type theory. Oxford University Press, 1990.
Bengt Nordström, Kent Petterson, Jan Smith. Martin-Löf’s Type Theory. Handbook of Logic in Computer Science, OUP, 2000.

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.
Alan Jeffrey, Agda introductory demo (dead link). A demo of Agda and its Emacs mode given to UIC’s undergraduate Advanced Programming Seminar. Source file
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

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.

This is a list of courses which use Agda. Please add your own!

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.
Seminar on Dependently Typed Programming, course at Utrecht University by Andres Löh.
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. (More info and feedback).
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.