I’ve written a draft paper describing the implementation of Idris, Implementation of a General Purpose Programming Language with Dependent Types, abstract as follows: Many components of a dependently typed programming language are by now well understood, for example the underlying type theory, type checking, unification and evaluation. How to combine these components into a realistic [...]

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…

My goal for Idris is to make it a practical dependently typed programming language – suitable for general purpose, systems programming, with precise types when you need them for increasing confidence in correctness of your program. One thing that a modern, practical language really needs, however, is a sane, safe, general way of overloading functions. [...]

A new draft, Resource-safe Systems Programming with Embedded Domain Specific Languages, by Edwin Brady and Kevin Hammond, submitted September 2011. We introduce a new overloading notation that facilitates programming, modularity and reuse in Embedded Domain Specific Languages (EDSLs), and use it to reason about safe resource usage and state management. We separate the structural language [...]

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