Last Friday I gave a talk at Scottish Theorem Proving in which I sketched how Idris worked. Here are the slides. There’ll be a paper explaining in more detail at some point fairly soon…

Slides from my invited talk at DTP 2011 are now available. In this talk, I give a brief introduction to the Idris programming language, and show how it can be used to implement embedded domain specific languages (EDSLs) with strong correctness properties. I introduce a dsl construct which gives these EDSLs a usable (i.e. readable [...]