Documentation

Release Notes

Manuals

• User Manual
• A list of books and tutorials
• Developers manual

HowTo

• How to install Agda on Windows Subsystem for Linux (WSL) (Nov 2019)
• How to input Unicode characters in Emacs:
  • Using the Agda input method
  • Using abbreviation mode
  • Using XCompose
• 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.

Papers using Agda

Courses using Agda

This page has been moved to https://agda.readthedocs.io/en/latest/getting-started/tutorial-list.html#courses-using-agda

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.
• Anton Setzer's links on Agda