External Resources

A collection of external resources concerning Idris mostly videos. If you know of a resource that hasn't been linked here please add it.

Disclaimer some of these materials were developed referencing earlier versions of Idris. Things change, so please bear this in mind when consuming the material. Where possible the most suitable released version (on hackage) of Idris used has been referenced.

Title	Description	Date	Version of Idris
Idris: verifying a monoid	Ensuring an instance of the Monoid type-class actually satisfies the "monoid laws" (i.e. associativity, left identity and right identity) using Idris, a dependently typed programming language.	2014-04-27	0.9.12
Idris: Type safe printf	Demonstrating creation of a type safe printf function using Idris, a dependently typed programming language.	2014-04-22	0.9.12
Dependently Typed Programming in Idris: A Demo	David Christiansen gave a talk at a Haskell DC meet-up.	2014-03-26	0.9.12
Idris: General Purpose Programming with Dependent Types	Edwin Brady gave a talk at a Haskell London meet-up.	2014-01-20	0.9.10
Scala vs. Idris	Miles Sabin and Edwin Brady exemplify what can be done with a language with dependent types, what are the limitations and what could be done in the future when dependent types reach maturity.	2013-09-20	0.9.9.1
Idris Mini Course at ITU	Edwin Brady gave a course on Dependently Typed Functional Programming in Idris at IT University, Copenhagen.	2013-03-11	0.9.7