A type-correct, stack-safe, provably correct, expression compiler

Conventional approaches to compiler correctness, type safety and type preservation have focused on off-line proofs, either on paper or formalised with a machine, of existing compilation schemes with respect to a reference operational semantics. This pearl shows how the use of dependent types in programming, illustrated here in Epigram, allows us not only to build-in these properties, but to write programs which guarantee them by design and subsequent construction. We focus here on a very simple expression language, compiled into tree-structured code for a simple stack machine. Our purpose here is not to claim any sophistication in the source language being modelled, but to show off the metalanguage as a tool for writing programs for which the type preservation and progress theorems are self-evident by construction, and finally, whose correctness can be proved directly in the system. In this simple setting we achieve the following; • a type-preserving evaluation semantics, which takes typed expressions to typed values. • a compiler, which takes typed expressions to stack-safe intermediate code. • an interpreter for compiled code, which takes stack-safe intermediate code to a big-step stack transition. • a compiler correctness proof, described via a function whose type expresses the equational correctness property.