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
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.
The homepage of Agda
is a Wiki at Chalmers.
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.
. We will mainly
use the tutorial by Ulf Norell.
- 23 Apr 2013