[Agda] Dependent Types at Work

[Peter Dybjer]

Ana Bove and I have written a tutorial on dependently typed programming in
Agda:

http://www.cs.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf

It is not self-contained and only deals with some of the features of Agda.
But it may serve as a complement to other documentation, especially for
people with little previous experience of dependent types.

We used it at the LerNet summer school in Uruguay two weeks ago. We will
prepare a final version later this spring, which is planned to appear in
Springer Tutorial Series together with other course notes from the summer
school. So any feedback you might have will be useful for preparing this
final version.

Peter