Agda

DTP
The programming language we will use throughout the second part of this course.

Agda2 is a dependently typed programming language with a specific focus on
_programming_ rather than _theorem proving_. Of course, like other languages
based on dependent types, it allows to specify and prove properties. But currently,
there are more convenience features for writing executable programs than for
verifying complex properties.

---++ Homepage

The [[http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php][homepage of Agda]]
is a Wiki at Chalmers.

---++ Installation

Ideally, you can install Agda via Cabal. We will work with version 2.3.2 of Agda.

For further information,
there is a [[http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Main.Download][Wiki page]]
that explains how to install Agda. It also lists the required software.

---++ Tutorials

Look [[http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Othertutorials][here]]. We will mainly
use the tutorial by Ulf Norell.

-- Main.WouterSwierstra  - 23 Apr 2013