PLPV 2013 Slides

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

Posted January 22, 2013 by edwinb in Idris, Talks

%d bloggers like this: