TY - UNPD A1 - Schmidt-Schauß, Manfred A1 - Niehren, Joachim A1 - Schwinghammer, Jan A1 - Sabel, David T1 - Adequacy of compositional translations for observational semantics T2 - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 33 N2 - We investigate methods and tools for analyzing translations between programming languages with respect to observational semantics. The behavior of programs is observed in terms of may- and mustconvergence 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 extensions. T3 - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik - 33 [v.5] KW - Operationale Semantik KW - Lambda-Kalkül KW - Programmiersprache Y1 - 2009 UR - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/34433 UR - https://nbn-resolving.org/urn:nbn:de:hebis:30:3-344334 UR - http://www.ki.informatik.uni-frankfurt.de/papers/frank/frank-33_v5.pdf IS - Version: 28 Febr. 2009 EP - 23 PB - Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik CY - Frankfurt am Main ER -