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