inria-00257279, version 7
Adequacy of compositional translations for observational semantics
Manfred Schmidt-Schauß 1Joachim Niehren
2Jan Schwinghammer 3David Sabel 1
5th IFIP International Conference on Theoretical Computer Science 273 (2008) 521-535
Résumé : 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é Lille 1 - Sciences et Technologies : EA3588 – Université Charles de Gaulle - Lille III
- 3 : Programming Systems Lab [Saarland]
- Saarland University
- Domaine : Informatique/Langage de programmation
- Commentaire : Revised Version from October 2008
- Versions disponibles : v1 (19-02-2008) v2 (14-04-2008) v3 (08-08-2008) v4 (08-08-2008) v5 (05-09-2008) v6 (14-10-2008) v7 (02-03-2009)
- inria-00257279, version 7
- http://hal.inria.fr/inria-00257279
- oai:hal.inria.fr:inria-00257279
- Contributeur : Joachim Niehren
- Soumis le : Lundi 2 Mars 2009, 21:42:01
- Dernière modification le : Lundi 2 Mars 2009, 21:45:39
Documents associés
Exporter