Adequacy of Compositional Translations for Observational Semantics

Abstract. We investigate methods and tools for analyzing translations between programming languages with respect to observational seman-tics. The behavior 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 cor-rectness condition. For compositional translations we propose a notion of convergence equivalence as a means for proving adequacy. This tech-nique avoids explicit reasoning about contexts, and is able to deal with the subtle role of typing in implementations of language extensions.4