The project "Observational Correctness of Programming Language Translations" analyses the correctness of translations between programming languages. Those correctness proofs are needed in several fields of computer science. For instance, compilers translate high-level programming language into low-level languages and thus correctness of the translation ensures correctness of the compiler. Translations can also be used to obtain expressivity results for programming languages which help to classify programming languages. Correctly implementing new programming constructs as a programming library requires to show correctness of the implementation, which can be established by representing the implementation as a translation from an extended language into the original one.
As the notion of correctness we focus on observational correctness, which is built on top of the contextual semantics of programming languages. Since the formalism of contextual semantics can be defined for a wide range of programming languages, our approach has a broad scope.
On the one hand the research project aims to gain more knowledge on the foundations of translations and their correctness. On the other hand a significant part of the project is devoted to automatize the correctness proof for programming languages translations. To achieve the automation specific algorithms will be developed and implemented as a software tool. Finally, also a goal of the project is also to obtain new correctness results of translations for concurrency in imperative programming languages and also for functional programming languages and their extensions by concurrency.
