Dependently Typed Programming in Agda

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]

@inproceedings{Norell08,
  title = {Dependently Typed Programming in Agda},
  author = {Ulf Norell},
  year = {2008},
  doi = {10.1007/978-3-642-04652-0_5},
  url = {http://dx.doi.org/10.1007/978-3-642-04652-0_5},
  tags = {programming},
  researchr = {https://researchr.org/publication/Norell08},
  cites = {0},
  citedby = {0},
  pages = {230-266},
  booktitle = {Advanced Functional Programming, 6th International School, AFP 2008, Heijen, The Netherlands, May 2008, Revised Lectures},
  editor = {Pieter W. M. Koopman and Rinus Plasmeijer and S. Doaitse Swierstra},
  volume = {5832},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-04651-3},
}