David Sabel

Computer Scientist

Home Research Publications Talks Teaching Software

Research Project

Observational Correctness of Programming Language Translations


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.

Project Period

2016 - 2019

The project is funded by the German Research Foundation, grant SA 2908/3-1
Patrick Pech. Nominal Unification and its application for syntactic reasoning in extended lambda calculi. Master thesis, Goethe University Frankfurt am Main, 2016.
Manfred Schmidt-Schauß and David Sabel. Unification of program expressions with recursive bindings. In Germán Vidal, editor, PPDP '16: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, pages 160--173, New York, NY, USA, September 2016. ACM.
bib | DOI | http ]
David Sabel and Hans Zantema. TermComp 2016 Partipicant: cycsrs 0.2.
In Aart Middeldorp and René Thiemann, editors, Proceedings of the 15th International Workshop on Termination, Obergurgl, Austria, pages 21:1, 2016.
http ]
David Sabel and Hans Zantema. Termination of cycle rewriting by transformation and matrix interpretation. Logical Methods in Computer Science, Volume 13, Issue 1, March 2017.
bib | DOI | http ]
Manfred Schmidt-Schauß and David Sabel. Improvements in a call-by-need functional core language: Common subexpression elimination and resource preserving translations. Science of Computer Programming, 147:3--26, 2017.
bib | DOI | PDF | http ]
David Sabel. Rewriting of higher-order meta-expressions with recursive bindings. Frankfurter Informatik-Berichte 2017-1, Goethe-University Frankfurt am Main, 2017.
bib | http ]
David Sabel. Symbolic alpha-renaming for higher-order meta-expressions with recursive bindings. Frankfurter Informatik-Berichte 2017-2, Goethe-University Frankfurt am Main, 2017.
bib | http ]
David Sabel. Matching of Meta-Expressions with Recursive Bindings In UNIF'17: International Workshop on Unification, September 2017,
bib | http ]
David Sabel. Alpha-renaming of higher-order meta-expressions. In Brigitte Pientka and Wim Vanhoof, editors, Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, PPDP '17, pages 151--162, New York, NY, USA, 2017. ACM. ©ACM.
bib | DOI | PDF | http ]
Manfred Schmidt-Schauß, David Sabel, and Yunus Kutz. Nominal unification with atom-variables. J. Symbolic Comput., 2017. accepted for publication, to appear.
bib | PDF ]
Principal Investigator
PD Dr. David Sabel
PD Dr. David Sabel
Computer Science Institute
Computer Science and Mathematics Department
Johann Wolfgang Goethe-University Frankfurt am Main
(c) 2016 PD Dr. David Sabel, Imprint, Last modified: $Author: sabel $, $Date: 2017/10/17 13:23:18 $