Idris: General Purpose Programming with Dependent Types

A great talk by the creator of Idris, Edwin Brady. Slides here (but you miss out on the demo): http://eb.host.cs.st-andrews.ac.uk/writings/idris-lhug0113.p...

http://idris-lang.org/