WG211/M8Brady

Implementing Domain Specific Languages using Dependent Types and Partial Evaluation

Ed Brady

In this talk, I will describe the efficient implementation of domain specific languages (DSLs) in Idris, a dependently typed functional
programming language. I will show how Idris can be used to implement a verified network transport protocol, as a DSL. I will present experimental evidence that partial evaluation of such programs yields efficient residual programs whose performance is competitive with their Java and C equivalents and which are also, through the use of dependent types, verifiably type- and resource-safe.