nLab Ulf Norell

• webpage

Selected writings

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:

• Ulf Norell, Programming in Agda, presentation at Oregon Programming Languages Summer School (2014) [lecture 1: video, 2: video, 3: video, 4: video]

Related entries

• Agda

category: people