Skip to Main content Skip to Navigation
New interface
Conference papers

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.
Complete list of metadata

Cited literature [10 references]  Display  Hide  Download
Contributor : Nicolas Tabareau Connect in order to contact the contributor
Submitted on : Tuesday, May 24, 2011 - 5:07:24 PM
Last modification on : Wednesday, April 27, 2022 - 4:21:24 AM
Long-term archiving on: : Friday, November 9, 2012 - 12:06:01 PM


Files produced by the author(s)


  • HAL Id : hal-00594386, version 1


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⟩



Record views


Files downloads