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.
Liste complète des métadonnées

Cited literature [10 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-00594386
Contributor : Nicolas Tabareau <>
Submitted on : Tuesday, May 24, 2011 - 5:07:24 PM
Last modification on : Wednesday, December 5, 2018 - 1:22:12 AM
Document(s) archivé(s) le : Friday, November 9, 2012 - 12:06:01 PM

File

lola2011.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

786

Files downloads

173