The Journey of Biorthogonal Logical Relations to the Realm of Assembly Code

Guilhem Jaber 1, 2, 3 Nicolas Tabareau 2, 3
2 ASCOLA - Aspect and composition languages
LINA - Laboratoire d'Informatique de Nantes Atlantique, Département informatique - EMN, Inria Rennes – Bretagne Atlantique
Abstract : Logical relations appeared to be very fruitful for the development of modular proofs of compiler correctness. In this field, logical relations are parametrized by a high-level type system, and are even sometimes directly relating low level pieces of code to high-level programs. All those works rely crucially on biorthogonality to get extensionality and compositionality properties. But the use of biorthogonality in the definitions also complicates matters when it comes to operational correctness. Most of the time, such correctness results amount to show an unfolding lemma that makes reduction more explicit than in a biorthogonal definition. Unfortunately, unfolding lemmas are not easy to derive for rich languages and in particular for assembly code. In this paper, we focus on three different situations that enable to reach step-by-step the assembly code universe: the use of Curry-style polymorphism, the presence of syntactical equality in the language and finally an ideal assembly code with a notion of code pointer.
Type de document :
Communication dans un congrès
Workshop LOLA 2011, Syntax and Semantics of Low Level Languages, Jun 2011, Toronto, Canada
Liste complète des métadonnées

https://hal.archives-ouvertes.fr/hal-00594386
Contributeur : Nicolas Tabareau <>
Soumis le : mardi 24 mai 2011 - 17:07:24
Dernière modification le : jeudi 9 février 2017 - 15:30:10
Document(s) archivé(s) le : vendredi 9 novembre 2012 - 12:06:01

Fichier

lola2011.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00594386, version 1

Citation

Guilhem Jaber, Nicolas Tabareau. The Journey of Biorthogonal Logical Relations to the Realm of Assembly Code. Workshop LOLA 2011, Syntax and Semantics of Low Level Languages, Jun 2011, Toronto, Canada. <hal-00594386>

Partager

Métriques

Consultations de
la notice

377

Téléchargements du document

117