This week I’ve been giving a course on Dependently Typed Functional Programming in Idris at IT University, Copenhagen. Various course materials are available:

• Lecture 1, Introduction, slides, video
• Lecture 2, Embedded DSLs, slides, video
• Lecture 3, Effect management, slides, video
• Lecture 4, Implementing Idris, slides, video
• Example code
• Exercises
• Idris web page

I have put slides from my PLPV 2013 invited talk online here. You can also find the example code.

Of course, the slides won’t make as much sense as with the accompanying commentary, but at least you’ll see what I talked about, and maybe you’ll get something from them anyway. In them, you’ll find:

• An introduction to Idris
• Some examples: verified binary arithmetic, lightweight verification of a virtual machine, and
  my plan to never have to write a monad transformer again.

• Some notes on compilation issues

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 and writable) concrete syntax, and show how it can be used to tackle realistic resource management problems in systems programming.

Code for the resource management EDSL is on github, though I don’t promise much in the way of comments or documentation yet. There is a paper on the way soon which will explain the gory details.

(Usual disclaimer for publishing slides: you really need the talk as well as the slides to understand all of the details, so questions and comments are more than welcome.)