zbMATH — the first resource for mathematics

Dependently typed programming in Agda. (English) Zbl 1263.68038
Koopman, Pieter (ed.) et al., Advanced functional programming. 6th international school, AFP 2008, Heijen, The Netherlands, May 2008. Revised lectures. Berlin: Springer (ISBN 978-3-642-04651-3/pbk). Lecture Notes in Computer Science 5832, 230-266 (2009).
Summary: In Hindley-Milner style languages, such as Haskell and ML, there is a clear separation between types and values. In a dependently typed language the line is more blurry – types can contain (depend on) arbitrary values and appear as arguments and results of ordinary functions.
For the entire collection see [Zbl 1176.68009].

68N18 Functional programming and lambda calculus
Full Text: DOI
[1] The Agda mailing list (2008), https://lists.chalmers.se/mailman/listinfo/agda
[2] The Agda wiki (2008), http://www.cs.chalmers.se/ ulfn/Agda
[3] Altenkirch, T., McBride, C., McKinna, J.: Why dependent types matter. Manuscript (April 2005)
[4] McBride, C., McKinna, J.: The view from the left. Journal of Functional Programming 14(1), 69–111 (2004) · Zbl 1069.68539 · doi:10.1017/S0956796803004829
[5] Norell, U.: Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden (September 2007)
[6] Oury, N., Swierstra, W.: The power of pi. In: Accepted for presentation at ICFP (2008) · Zbl 1323.68145 · doi:10.1145/1411204.1411213
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.