An automatically generated and provably correct compiler for a subset of Ada

We describe the automatic generation of a provably correct compiler for a non-trivial subset of Ada. The compiler is generated from an emantic description; it emits absolute code for an abstract RISC 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 Mosses, Paulson, and Wand. The use of action semantics makes the processable language specification easy to read and pleasant to work with. In Proc. ICCL'92, Fourth IEEE International Conference on Computer Languages, pages 117

• Type: Conference
• Year: 1992
• Where: ICCL
• Authors: Jens Palsberg
• Keywords: Compilers, Generated Code, ICCL 1992, Programming Languages, RISC Machine Language