KIT | KIT-Bibliothek | Impressum | Datenschutz

Proving compiler correctness with evolving algebra specifications

Beckert, Bernhard ORCID iD icon; Haehnle, Reiner


The purpose of this note is to define a framework for proving
compiler correctness with evolving algebra (EA) specifications.
Although our specific domain is the verification of a Prolog-to-WAM
compiler, we think that our considerations are fairly general and
they should be useful in other areas as well.

First we define our general view of the semantics of a programming
language, of how semantics can be specified using EAs, and of
compiler correctness; then we describe how the correctness of a
compiler may be proven; and finally we point out the differences
to the approach of Egon Boerger and Dean Rosenzweig and to the
notion of correctness as commonly used in logic.

Volltext §
DOI: 10.5445/IR/21796
Cover der Publikation
Zugehörige Institution(en) am KIT Fakultät für Informatik – Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Publikationstyp Buch
Publikationsjahr 1996
Sprache Englisch
Identifikator urn:nbn:de:swb:90-AAA217960
KITopen-ID: 21796
Erscheinungsvermerk Karlsruhe 1996. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1996,4.)
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page