On Friday October 17, this site was moved to a new server, https://mw.hh.se. The original address will continue to work. Whithin a week or two this site will return to the original address. /Peo HH IT-dep
WG211/M8Brady: Difference between revisions
From WG 2.11
Jump to navigationJump to search
m 1 revision |
(No difference)
|
Latest revision as of 12:06, 12 December 2011
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.
