|
|
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
-
- [PP16]
-
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,
[ 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 ]
- Principal Investigator
-
PD Dr. David Sabel
- Contact
-
PD Dr. David Sabel
Computer Science Institute
Computer Science and Mathematics Department
Johann Wolfgang Goethe-University Frankfurt am Main
|
