David Sabel

Research Project: Observational Correctness of Programming Language Translations

Summary

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

Funding

The project is funded by the German Research Foundation, grant SA 2908/3-1

Publications

[Pec16]: Patrick Pech. Nominal Unification and its application for syntactic reasoning in extended lambda calculi. Master thesis, Goethe University Frankfurt am Main, 2016.
[SSS16]: 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 ]
[SZ16a]: 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 ]
[SZ16b]: 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 ]
[SSS17]: 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 ]
[Sab17a]: David Sabel. Rewriting of higher-order meta-expressions with recursive bindings. Frankfurter Informatik-Berichte 2017-1, Goethe-University Frankfurt am Main, 2017.
[ bib | http ]
[Sab17b]: 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 ]
[Sab17c]: David Sabel. Matching of Meta-Expressions with Recursive Bindings In UNIF'17: International Workshop on Unification, September 2017,
[ http ]
[Sab17d]: 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 ]
[Tre18]: Kristina Tretiak. Funktionale Implementierung von Lösungsverfahren für Non-Capture und Freshness Constraints in Higher-Order Sprachen
Master thesis, Goethe University Frankfurt am Main, 2018.
[SSS18]: Manfred Schmidt-Schauß and David Sabel. Nominal unification with atom and context variables. In Hélène Kirchner, editor, 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9-12, 2018, Oxford, UK, volume 108 of LIPIcs, pages 28:1--28:20. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, July 2018.
[ bib | DOI | http ]
[SSSD18]: Manfred Schmidt-Schauß, David Sabel, and Nils Dallmeyer. Sequential and parallel improvements in a concurrent functional programming language. In David Sabel and Peter Thiemann, editors, Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP '18, pages 20:1--20:13, New York, NY, USA, September 2018. ACM.
[ bib | DOI | http ]
[Sab19]: David Sabel. Automating the diagram method to prove correctness of program transformations. In Joachim Niehren and David Sabel, editors, Proceedings Fifth International Workshop on Rewriting Techniques for Program Transformations and Evaluation, Oxford, England, 8th July 2018, volume 289 of Electronic Proceedings in Theoretical Computer Science, pages 17--33. Open Publishing Association, February 2019.
[ bib | DOI | PDF ]
[SSSK19]: Manfred Schmidt-Schauß, David Sabel, and Yunus D. K. Kutz. Nominal unification with atom-variables. J. Symb. Comput., 90:42--64, 2019.
[ bib | DOI | PDF | http ]
[Ler19]: Peter Lermann. Automatisches Widerlegen der Beobachtungskorrektheit von Programmiersprachenübersetzungen
Master thesis, LMU Munich, 2019.
[Bau19]: Inga Baumgartner. Entwurf und Implementierung eines Unifikationsverfahrens für Gleichungen zwischen Multimengen von Bindungen
Bachelor thesis, Goethe-University Frankfurt, 2019
[Yos20]: Taro Yoshioka. On the Unification of Multiset-Equations of Variable-to-Variable Bindings
Bachelor thesis, LMU Munich, 2020.
[SSS20a]: Manfred Schmidt-Schauß and David Sabel. Embedding the pi-calculus into a concurrent functional programming language. Frank report 60, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, May 2020.
[ bib | PDF ]
[SSS20b]: Manfred Schmidt-Schauß and David Sabel. On Impossibility of Simple Modular Translations of Concurrent Calculi. 7th International Workshop on Rewriting Techniques for Program Transformations and Evaluation, 2020.

Principal Investigator

David Sabel