Publication details

Saarland University Computer Science

Correctness of Program Translations for Observational Semantics

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

Draft, November 2010

We investigate methods and tools to analyze translations between programming languages with respect to observational semantics. We consider a framework where the behavior of programs is observed by (possibly multiple) convergence predicates in arbitrary contexts. While observational correctness is taken to be the fundamental notion of correctness of a translation, we emphasize the role of other correctness conditions like adequacy and full abstraction of translations. As a tool for proving these correctness properties, we propose a notion of convergence equivalence as a means for proving adequacy for compositional translations which avoids explicit reasoning about contexts.

Revised and expanded version of IFIP TCS paper.

Download PDF        Show BibTeX               


Login to edit


Webmaster, Wed Sep 16 10:47:00 2009