# Documentation

## Release Notes

## Manuals

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

## Books

- Verified Functional Programming in Agda, by Aaron Stump, ACM Books, 2016. Available for purchase at Morgan and Claypool (publishers), Amazon, and others.

## HowTo

- How to input Unicode characters in Emacs:
- Emacs mode key combinations
- Editing Agda code using Vim
- How to see Unicode characters
- Literate Agda (or how to include Agda code in LaTeX documents)
- How to generate web pages from source code
- How to use automatic proof search (C-c C-a)
- How to cope with performance issues

## Publications

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

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

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

## Papers using Agda

## Courses using Agda

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.
- 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 (CS410), Conor McBride, Strathclyde, Fall 2013.
- 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.

## Small case studies

- Ali Onaissi.
*Prime numbers - a case study in the Interactive Theorem Prover Agda*. MSc thesis supervised by Anton Setzer, Swansea University, 2015.

## Misc

Agda has a wikipedia page.