Sciweavers

ESOP
1992
Springer

A Provably Correct Compiler Generator

13 years 7 months ago
A Provably Correct Compiler Generator
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.
Jens Palsberg
Added 10 Aug 2010
Updated 10 Aug 2010
Type Conference
Year 1992
Where ESOP
Authors Jens Palsberg
Comments (0)