-
Notifications
You must be signed in to change notification settings - Fork 642
External Resources
David Christiansen edited this page May 26, 2015
·
22 revisions
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 |
---|---|---|---|
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 |
Binary Packages
Tool Support
Community
- Libraries, available elsewhere
- Idris Developer Meetings
- The Zen of Idris
- Non English Resources
Development