Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

Adequacy of Compositional Translations for Observational Semantics

Manfred Schmidt-Schauß, Joachim Niehren, David Sabel, Jan Schwinghammer

5th IFIP International Conference on Theoretical Computer Science, Springer, September 2008

We investigate methods and tools for analysing translations between programming languages with respect to observational semantics. The behaviour of programs is observed in terms of may- and must-convergence in arbitrary contexts, and adequacy of translations, i.e., the reflection of program equivalence, is taken to be the fundamental correctness condition. For compositional translations we propose a notion of convergence equivalence as a means for proving adequacy. This technique avoids explicit reasoning about contexts, and is able to deal with the subtle role of typing in implementations of language extension.

Download PDF        Show BibTeX               

@INPROCEEDINGS{Schmidt-Schauss:Niehren:Schwinghammer:Sabel:08,
  title = {Adequacy of Compositional Translations for Observational Semantics},
  author = {Manfred Schmidt-Schauß and Joachim Niehren and David Sabel and Jan Schwinghammer},
  year = {2008},
  month = {sep},
  publisher = {{Springer}},
  booktitle = {5th IFIP International Conference on Theoretical Computer Science},
}

Login to edit