A type-correct, stack-safe, provably correct expression compiler in Epigram Export

@inproceedings{citeulike:3150500, 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 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. 1}, author = {Mckinna, James and Wright, Joel}, booktitle = {in the Journal of Functional Programming}, citeulike-article-id = {3150500}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.105.4086}, keywords = {language-epigram, lecture-cs-252r}, posted-at = {2008-08-23 08:33:17}, priority = {0}, title = {A type-correct, stack-safe, provably correct expression compiler in Epigram}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.105.4086}, volume = {2006}, year = {2006} }

TY - CONF ID - citeulike:3150500 L3 - citeulike-article-id:3150500 N2 - 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 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. 1 TI - A type-correct, stack-safe, provably correct expression compiler in Epigram VL - 2006 T2 - in the Journal of Functional Programming KW - language-epigram KW - lecture-cs-252r AU - Mckinna, James AU - Wright, Joel PY - 2006/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.105.4086 ER -