David Sabel


Computer Scientist


Home Research Publications Talks Teaching Software
EN

Forschungsprojekt

Beobachtungskorrektheit von Programmiersprachenübersetzungen

Zusammenfassung

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.

Projektzeitraum

2016 - 2019

Finanzierung
Das Projekt wird durch die Deutsche Forschungsgemeinschaft unter der Projektnummer SA 2908/3-1 gefördert.
DFG
Veröffentlichungen
[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.
Projektleitung
PD Dr. David Sabel
Kontakt
PD Dr. David Sabel
Institut für Informatik
Fachbereich Informatik und Mathematik
Johann Wolfgang Goethe-Universität Frankfurt am Main
©  David Sabel, Imprint, Privacy Policy