Further Reading

Further information about Idris programming, and programming with dependent types in general, can be obtained from various sources:

• Type-Driven Development with Idris by Edwin Brady, available from Manning.

• The community Idris2 tutorial, originally written by Stefan Höck, now maintained by the community.

• The Idris website (https://www.idris-lang.org/) has pointers to a broad range of resources.

• By asking questions on the discord server, or the mailing list (the discord server is currently the most active place for interactive discussion).

• The IRC channel #idris, on libera.chat.

• The wiki (idris-lang/Idris2) has further user provided information, in particular:

  • idris-lang/Idris2

  • idris-lang/Idris2

  • idris-lang/Idris2

• Existing projects on the Idris Community web space:

  • idris-community

• The papers describing Idris2 [1] and the older Idris1 [2] [3]. There is a wider (non-exhaustive) list of papers involving Idris on the website.

[1]

Edwin Brady. Idris 2: Quantitative Type Theory in Practice. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 9:1-9:26, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ECOOP.2021.9

[2]

E. BRADY, “Idris, a general-purpose dependently typed programming language: Design and implementation,” Journal of Functional Programming, vol. 23, no. 5, pp. 552-593, 2013. doi:10.1017/S095679681300018X https://doi.org/10.1017/S095679681300018X

[3]

Edwin C. Brady. 2011. IDRIS —: systems programming meets full dependent types. In Proceedings of the 5th ACM workshop on Programming languages meets program verification (PLPV ‘11). ACM, New York, NY, USA, 43-54. DOI=10.1145/1929529.1929536 https://doi.acm.org/10.1145/1929529.1929536