A verified staged interpreter is a verified compiler

Abstract

Dependent types and multi-stage programming have both been used, separately, in programming language design and implementation. 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 the combination of these techniques. We implement an interpreter for a simply typed lambda calculus, using dependent types to guarantee correctness properties by construction. We give explicit proofs of these correctness properties, then add staging annotations to generate a translator from the interpreter. In this way, we have constructed a verified compiler from a verified staged interpreter. We illustrate the application of the technique by considering a simple staged interpreter that provides guarantees for some simple resource bound properties, as might be found in a domain specific language for real-time embedded systems.