Introducing the dependently typed proof assistant/programming language 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]
Introduction:
Last revised on February 15, 2023 at 18:57:25. See the history of this page for a list of all contributions to it.