We investigate methods and tools to analyze translations
between programming languages with respect to
We consider a framework where the behavior of programs is
observed by (possibly multiple) convergence predicates in arbitrary
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
Revised and expanded version of IFIP TCS paper.
Download PDF Show BibTeX
Login to edit
Wed Sep 16 10:47:00 2009