[Agda] Dependent Types at Work

[Peter Dybjer]

I have also added a link to it on the Agda wiki.

Peter

> 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
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>