Documentation

Idris 2

Idris 2 is still a work in progress, but documentation is growing, and available from https://idris2.readthedocs.org. This includes:

There is API documentation for the following packages:

You can also find our Community Standards here.

Documentation for Idris 1 is available from https://docs.idris-lang.org.

There is API documentation for the following packages provided as part of the Idris distribution:

The Idris Wiki contains a lot of community supplied information.

There are several academic publications associated with Idris, including:

Value Dependent Session Design in a Dependently Typed Language, Jan de Muijnck-Hughes, Wim Vanderbauwhede and Edwin Brady, PLACES 2019
Automatically Proving Equivalence by Type-Safe Reflection, Franck Slama and Edwin Brady, Conference on Intelligent Computer Mathematics (CICM) 2017
Type-driven Development of Concurrent Communicating Systems, Edwin Brady, Computer Science Journal (AGH University of Science and Technology) 2017
Elaboration Reflection: Extending Idris in Idris, David Christiansen and Edwin Brady In proceedings of ICFP 2016
Resource-dependent Algebraic Effects, Edwin Brady In proceedings of TFP 2014
Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation, Edwin Brady In Journal of Functional Programming, October 2013.
Dependent Type Providers, David Christiansen In Workshop on Generic Programming, 2013.
Dependent Types for Safe and Secure Web Programming, Simon Fowler and Edwin Brady In proceedings of IFL 2013
Programming and Reasoning with Algebraic Effects and Dependent Types, Edwin Brady In proceedings of ICFP 2013
Idris – Systems Programming meets Full Dependent Types, Edwin Brady In proceedings of PLPV 2011.
Scrapping your Inefficient Engine: using Partial Evaluation to Improve Domain-Specific Language Implementation, Edwin Brady and Kevin Hammond In proceedings of ICFP 2010.