Agda

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 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 Wiki page that explains how to install Agda. It also lists the required software.

Tutorials

Look here. We will mainly use the tutorial by Ulf Norell.

-- WouterSwierstra - 23 Apr 2013