School of Computer Science
University of St Andrews
Thursday, 7 January 2010, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Slides from the talk [pdf]
Abstract: 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 that partial evaluation can be an effective and, unusually, straightforward technique for the efficient implementation of DSLs. We achieve this by exploiting dependent types and by following some simple rules in the definition of the DSL interpreter. I will present experimental evidence that partial evaluation of programs in domain-specific languages 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 resource-safe. Using this technique, it follows that a verifiably correct and resource-safe program can also be an efficient program.