Archive for the ‘Talks’ Category

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 [...]

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

Follow

Get every new post delivered to your Inbox.