Edwin Brady gave a talk on programming with dependent types in Idris at CodeMesh 2013 in December 2013. You can now see a video of the talk.