HAL - INRIA :: [inria-00257279, version 7] Adequacy of compositional translations for observational semantics

inria-00257279, version 7

Adequacy of compositional translations for observational semantics

Manfred Schmidt-Schauß ¹, Joachim Niehren () ², Jan Schwinghammer ³, David Sabel ¹

5th IFIP International Conference on Theoretical Computer Science 273 (2008) 521-535

Abstract: 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.

1: J. W. Goethe-Universitat
J. W. Goethe-Universitat
2: MOSTRARE (INRIA Lille - Nord Europe)
INRIA – CNRS : UMR8022 – Université des Sciences et Technologies de Lille - Lille I : EA3588 – Université Charles de Gaulle - Lille III
3: Programming Systems Lab [Saarland]
Saarland University

inria-00257279, version 7
http://hal.inria.fr/inria-00257279
oai:hal.inria.fr:inria-00257279
From: Joachim Niehren <>
Submitted on: Monday, 2 March 2009 21:42:01
Updated on: Monday, 2 March 2009 21:45:39

See detailed view

Associated documents

PDF :

Export

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="inproceedings"><head>Peer-reviewed conferences/proceedings</head>
<biblStruct type="inproceedings" xml:id="inria-00257279"><analytic>
<author><persName><forename>Manfred</forename><surname>Schmidt-Schauß</surname></persName>
<affiliation>
<orgName type="team">J. W. Goethe-Universitat</orgName>
<country>DE</country>
<orgName type="institution">J. W. Goethe-Universitat</orgName>
</affiliation>
</author>
<author><persName><forename>Joachim</forename><surname>Niehren</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lille - Nord Europe</orgName>
<orgName type="team">MOSTRARE</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR8022</orgName>
<orgName type="institution">Université des Sciences et Technologies de Lille - Lille I : EA3588</orgName>
<orgName type="institution">Université Charles de Gaulle - Lille III</orgName>
</affiliation>
</author>
<author><persName><forename>Jan</forename><surname>Schwinghammer</surname></persName>
<affiliation>
<orgName type="team">Programming Systems Lab [Saarland]</orgName>
<country>DE</country>
<orgName type="institution">Saarland University</orgName>
</affiliation>
</author>
<author><persName><forename>David</forename><surname>Sabel</surname></persName>
<affiliation>
<orgName type="team">J. W. Goethe-Universitat</orgName>
<country>DE</country>
<orgName type="institution">J. W. Goethe-Universitat</orgName>
</affiliation>
</author>
<title type="main" level="a">Adequacy of compositional translations for observational semantics</title></analytic><monogr><meeting>5th IFIP International Conference on Theoretical Computer Science</meeting><imprint><publisher>Springer Verlag</publisher><pubPlace><settlement>Milano</settlement><country>Italy</country></pubPlace><biblScope type="publicationDate">2008-00-00</biblScope><biblScope type="vol">273</biblScope><biblScope type="pp">521-535</biblScope></imprint></monogr><idno type="HALid">http://hal.inria.fr/inria-00257279</idno><idno type="HALFile">http://hal.inria.fr/inria-00257279/PDF/0.pdf</idno></biblStruct>
</listBibl>
</listBibl>