Hi Everyone, It is my pleasure to announce the immediate availability of a Functional Pearl entitled "A type-correct, stack-safe, provably correct, expression compiler in Epigram", which will shortly be submitted to the Journal of Functional Programming.
The abstract is included below, and the full paper and program source can be found at "http://www.cs.nott.ac.uk/~jjw"; (also on "http://www.e-pig.org/"; soon). We hope you enjoy it, Joel Wright and James McKinna. ---------------- --- ABSTRACT --- ---------------- 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 a typed expression to a typed value. * a compiler, which takes a typed expression 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.
