.. _sect-concs:

***************
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 <https://www.manning.com/books/type-driven-development-with-idris>`_
   by Edwin Brady, available from `Manning <https://www.manning.com>`_.

*  `The community Idris2 tutorial <https://idris-community.github.io/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 <https://discord.gg/UX68fDs2jc>`_,
   or `the mailing list <https://groups.google.com/forum/#!forum/idris-lang>`_
   (the discord server is currently the most active place for interactive
   discussion).

*  The IRC channel ``#idris``, on
   `libera.chat <https://libera.chat/>`__.

*  The wiki (https://github.com/idris-lang/Idris2/wiki) has further
   user provided information, in particular:

   * https://github.com/idris-lang/Idris2/wiki/Resources

   * https://github.com/idris-lang/Idris2/wiki/Editor-Support

   * https://github.com/idris-lang/Idris2/wiki/Third-party-Libraries

*  Existing projects on the ``Idris Community`` web space:

   * https://github.com/idris-community

*  The papers describing Idris2 [#Brady2021]_ and the older Idris1
   [#Brady2013]_ [#Brady2011]_.  There is a wider (non-exhaustive) list of
   papers involving Idris
   `on the website <https://www.idris-lang.org/pages/papers.html>`_.


.. [#Brady2021] 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

.. [#Brady2013] 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 

.. [#Brady2011] 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
