A type correct, provably correct expression compiler: a case study in EPIGRAM

Dr James McKinna, University of St Andrews

Conventional approaches to compiler correctness, since McCarthy's pioneering studies, have focused on off-line proofs of correctness, on paper or formalised with a machine, of existing compilation schemes with respect to a reference operational semantics given by eval(whether specified relationally or as a functional program). Indeed, the related scenario of type preservation for source languages such as ML, posits a property of the run-time semantics vis-a-vis the compile-time semantics. Existing typed intermediate languages for compilation, such as TIL, FLINT, and proofs of correctness of compilation into them, still rest on this basic paradigm.

Dependently-typed languages, such as DML, Cayenne, or the logic programming frameworks of Pfenning et al., allow us to build type preservation directly into the representation of object language abstract syntax, as well as directly providing a theorem-proving surface via propositions-as-types. The synthesis of these two approaches gives rise to an illustrative development in Epigram of a simple expression language with conditionals, comprising:

• eval, which takes a typed expression to a typed value;
• compile, which takes a type expression to stack-safe intermediate code;
• exec, which takes stack-safe intermediate code to a stack transition.

exec . compile = push . eval