Archive for the ‘Talks’ Category
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…
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.)