The Journey of Biorthogonal Logical Relations to the Realm of Assembly Code
Guilhem Jaber, Nicolas Tabareau · 2011
Abstract. Logical relations appeared to be very fruitful for the devel-opment 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 pro-grams. All those works rely crucially on biorthogonality to get exten-sionality 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 biorthog-onal 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 pres-ence of syntactical equality in the language and finally an ideal assembly code with a notion of code pointer.