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

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