|
|
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.
- Veröffentlichungen
-
- [PP16]
-
Patrick Pech.
Nominal Unification und ihre Anwendung zum syntaktischen Schließen in erweiterten Lambda-Kalkülen.
Masterarbeit, Goethe-Universität 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,
[ bib |
http ]
-
[Sab17d]
-
David Sabel.
Alpha-renaming of higher-order meta-expressions.
In Brigitte Pientka, editor, PPDP '17: Proceedings of the 19th
International Symposium on Principles and Practice of Declarative
Programming, New York, NY, USA, October 2017. ACM.
©ACM, to appear.
[ bib |
DOI |
PDF |
http ]
- 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
|
