On dependent type theory with Agda:
Ulf Norell, Towards a practical programming language based on dependent type theory, PhD thesis (2007) [pdf, pdf]
Ulf Norell, Dependently Typed Programming in Agda, p. 230-266 in: Advanced Functional Programming AFP 2008. Lecture Notes in Computer Science 5832 (2009) [doi:10.1007/978-3-642-04652-0_5, pdf]
Last revised on September 3, 2022 at 19:09:38. See the history of this page for a list of all contributions to it.