Ulf Norell. Dependently Typed Programming in Agda. In Pieter W. M. Koopman, Rinus Plasmeijer, S. Doaitse Swierstra, editors, Advanced Functional Programming, 6th International School, AFP 2008, Heijen, The Netherlands, May 2008, Revised Lectures. Volume 5832 of Lecture Notes in Computer Science, pages 230-266, Springer, 2008. [doi]