- How to install Agda on Windows Subsystem for Linux (WSL) (Nov 2019)
- 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
- 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.
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.
Powered by PmWiki