Das Projekt "Beobachtungskorrektheit von Programmiersprachenübersetzungen" hat zum Ziel, Übersetzungen zwischen Programmiersprachen als korrekt nachzuweisen. Der Beweis solcher Korrektheiten hat Anwendungen in vielen Bereichen der Informatik. Z.B. kann durch ihn sichergestellt werden, dass ein Compiler, der eine höhere Programmiersprache in eine maschinennahe Sprache übersetzt, bei der Übersetzung keine Fehler einbaut. Ebenso lassen sich durch solche Korrektheitsresultate verschiedene Programmiersprachen hinsichtlich ihrer Ausdruckskraft vergleichen und klassifizieren. Schließlich können auch Bibliotheksimplementierungen von neuen Programmierkonstrukten als Übersetzungen aufgefasst werden und daher kann mit dem Zeigen der Korrektheit solcher Übersetzungen der Nachweis der korrekten Implementierung geführt werden.
Als Korrektheitsbegriff steht die Beobachtungskorrektheit im Vordergrund, die auf der kontextuellen Semantik der Programmiersprachen aufbaut und daher für viele Programmiersprachen verwendet werden kann.
Im Rahmen des Projekts sollen einerseits grundlegende Erkenntnisse zu Übersetzungen und ihrer Korrektheit erforscht werden. Anderseits widmet sich das Projekt in großen Teilen der Automatisierung solcher Korrektheitsnachweise durch die Entwicklung von speziellen Algorithmen und der Implementierung eines entsprechenden Softwarewerkzeuges. Schließlich werden im Projekt konkrete Übersetzungen einerseits im Bereich
der imperativen nebenläufigen Programmiersprachen und andererseits im Bereich der funktionalen Programmiersprachen und ihrer Erweiterungen um nebenläufige Auswertung entworfen und bezüglich ihrer Korrektheit untersucht.
