Archive for the ‘Talks’ Category

Idris course at ITU, slides and video

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

Posted March 15, 2013 by edwinb in Dependent Types, Idris, Talks

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

Elaborating Idris – STP slides

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…

Posted February 13, 2012 by edwinb in Dependent Types, Idris, Talks

Systems Programming with Dependent Types at DTP11

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.)

Posted August 27, 2011 by edwinb in Dependent Types, Idris, Talks