Lambda the Ultimate

In the continuing story called Epigram, a new contribution by James mcKinna and Joel Wright.

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.

P.S. I found it difficult to classify this paper correctly. Neither functional, nor type theory seem the proper category for a dependently typed programming language, which probably is a separate paradigm.