Adequacy of compositional translations for observational semantics
- We investigate methods and tools for analysing translations between programming languages with respect to observational semantics. The behaviour 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 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 extension.
Volltext Dateien herunterladen
Version 19. February 2008
Version February 28, 2009
Version October 14, 2008
Version July 10, 2008
Version 15. April 2008
Weitere Dienste
| Verfasserangaben: | Manfred Schmidt-SchaußORCiDGND, Joachim Niehren, Jan Schwinghammer, David SabelORCiDGND |
|---|---|
| URN: | urn:nbn:de:hebis:30-53623 |
| URL: | http://www.ki.informatik.uni-frankfurt.de/papers/frank/frank-33.pdf |
| Titel des übergeordneten Werkes (Deutsch): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 33 |
| Schriftenreihe (Bandnummer): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (33) |
| Verlag: | Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik, Research group for Artificial Intelligence and Software Technology |
| Verlagsort: | Frankfurt [am Main] |
| Dokumentart: | Arbeitspapier |
| Sprache: | Englisch |
| Datum der Veröffentlichung (online): | 19.02.2008 |
| Datum der Erstveröffentlichung: | 19.02.2008 |
| Veröffentlichende Institution: | Universitätsbibliothek Johann Christian Senckenberg |
| Datum der Freischaltung: | 07.03.2008 |
| Freies Schlagwort / Tag: | lambda calculus; nondeterminism; programming languages; semantics; translation |
| GND-Schlagwort: | Lambda-Kalkül; Operationale Semantik; Programmiersprache |
| Ausgabe / Heft: | Version: 19. Febr. 2008 |
| Seitenzahl: | 19 |
| Letzte Seite: | 19 |
| HeBIS-PPN: | 195575067 |
| Institute: | Informatik und Mathematik / Informatik |
| DDC-Klassifikation: | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik |
| Lizenz (Deutsch): |  Deutsches Urheberrecht |
