Teaching‎ > ‎Aarhus Mini-course‎ > ‎

Software

We will be using the Agda proof assistant that is based on a version of Martin-Löf Type Theory.

Please come to class with your laptop with Agda pre-installed:
  • If you are using Debian testing (wheezy) of unstable (sid), simply install the package "agda";
  • Or, if you have the time to play around, you may install Agda from source;
  • But, to simplify your life, you can also download the Debian Live ISO image with Agda preinstalled from here, which you can either boot from directly, or run in VirtualBox. Note that you will need some kind of additional external storage, like a USB key or a virtual hard disk in VirtualBox to save changes from the live cd. Git is also installed in the live cd in case you want to use version control.

Agda works in Emacs. While one can get by by using the mouse and the menu in Emacs, it is advisable to go through the Emacs Turorial from the Help menu, if one is not used to it.

Comments