Adequacy of compositional translations for observational semantics

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.

Metadaten
Author:	Manfred Schmidt-Schauß ORCiD GND, Joachim Niehren, Jan Schwinghammer, David Sabel ORCiD GND
URN:	urn:nbn:de:hebis:30:3-344326
URL:	http://www.ki.informatik.uni-frankfurt.de/papers/frank/frank-33_v4.pdf
Parent Title (English):	Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 33
Series (Serial Number):	Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (33 [v.4])
Publisher:	Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik
Place of publication:	Frankfurt am Main
Document Type:	Working Paper
Language:	English
Date of Publication (online):	2008/10/14
Date of first Publication:	2008/10/14
Publishing Institution:	Universitätsbibliothek Johann Christian Senckenberg
Release Date:	2014/07/08
GND Keyword:	Operationale Semantik; Lambda-Kalkül; Programmiersprache
Issue:	Version: 14 Oktober 2008
Page Number:	21
Last Page:	21
HeBIS-PPN:	344379744
Institutes:	Informatik und Mathematik / Informatik
Dewey Decimal Classification:	0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Sammlungen:	Universitätspublikationen
Licence (German):	Deutsches Urheberrecht

Open Access