A Provably Correct Compiler Generator
DOI:
https://doi.org/10.7146/dpb.v21i382.6614Abstract
We have designed, implemented, and proved the correctness of a compiler generator that accepts action semantic descriptions of imperative programming languages. The generated compilers emit absolute code for an abstract RISC machine language that currently is assembled into code for the SPARC and the HP Precision Architecture. Our machine language needs no run-time type-checking and is thus more realistic than those considered in previous compiler proofs. We use solely algebraic specifications; proofs are given in the initial model.Downloads
Published
1992-01-01
How to Cite
Palsberg, J. (1992). A Provably Correct Compiler Generator. DAIMI Report Series, 21(382). https://doi.org/10.7146/dpb.v21i382.6614
Issue
Section
Articles
License
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.