Dependently Typed Meta-programming
Edwin C. Brady, Kevin L Hammond · 2006
Dependent types and multi stage programming have both been used, separately, as implementation techniques for programming languages. Each technique has its own advantages — with dependent types, we can verify aspects of interpreters and compilers such as type safety and stack invariants. Multi stage programming, on the other hand, can give the implementor access to underlying compiler technology; a staged interpreter is a translator. In this paper, we investigate how we might combine these techniques to implement a compiler for a resource-safe functional programming language for embedded systems.