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.

Articles

Title	Description	Date	Version of Idris
Short intro by F. Teegen	Seminar Article
Hello World in Idris	Simple Idris Hello World program in the Hello World Collection

Books

Title	Description	Date	Version of Idris
Type-Driven Development with Idris	by Edwin Brady (Manning Publications).	2015-09-15	1.0
Introduction to Dependent Types with Idris	by Boro Sitnikovski (Apress).	2023-03-17
Seven More Languages in Seven Weeks	Idris is one of the Seven Languages.	November 2014	0.9.14

Blogs, wikis

Title	Description	Date	Version of Idris
Idris learning diary	From the perspective of a newbee	2016	0.9.21 - 0.10.0

Videos

Title	Description	Date	Version of Idris
Dependent Types in Idris	Lectures at Oregon Programming Languages Summer School: Part 1, Part 2, Part 3, Part 4	June-July, 2017	1.0
Type-Driven Development	Talk by @edwinbrady at Big Techday 9	June, 2016	?
Type-Driven Development	Talk by @edwinbrady at Scala World 2015	October, 2015	0.9.20
Coding for Types: The Universe Patern in Idris	David Christiansen at Curry On	July 2015
Dependently Typed Programming in Idris	A series of three introductory talks with exercises	January, 2015	0.9.16
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