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
Programming with Dependent Types in Idris	@raichoo talks about Idris at 31C3	2014-12-29	0.9.15.1
Episode 2: Edwin Brady on Idris	@edwinb talks about Idris on the Type Theory Podcast.	2014-09-26	nvt
Idris: Practical Dependent Types with Practical Examples	A talk by @puffnfresh on Idris at The Strange Loop	2014-09-22	0.9.14.2
Tic Tac Type: Dependent Types with Idris	This talk will step through an end-to-end example in Idris, from fundamentals like building type-safe APIs, and performing IO through to building user interfaces.	2014-05-09	0.9.12
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