An automatically generated and provably correct compiler for a subset of Ada
Jens Palsberg · 2003
The automatic generation of a provably correct compiler for a nontrivial subset of Ada is described. The compiler is generated from an action semantic description; it emits absolute code for an abstract RISC (reduced instruction set computer) machine language that currently is assembled into code for the SPARC and the HP Precision Architecture. The generated code is an order of magnitude better than what is produced by compilers generated by the classical systems of P.D. Mosses, L. Paulson, and M. Wand. The use of action semantics makes the processable language specification easy to read and pleasant to work with.>