Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E
			   __
			  / _`  _   /  /  o
			 /   ) __) /  /  / /  / /\/|
			(___/ (_/ (_ (_ / (__/ /   |

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                            Salle A115, bâtiment A

                          Lundi 17 septembre, 10h30

                            ---------------------
                            Ramon Fernandez I Mir
                            ---------------------

                                    Inria

              ==================================================
              Formal Verification of Data Layout Transformations
              ==================================================

Data layout transformations such as array-of-structures to
structure-of-arrays, peeling and splitting of records, can lead to significant
performance improvement. Yet, these transformations are error-prone and hard
to debug. In this work, we aim at formalizing in Coq the correctness of such
transformations.

To that end, we consider a C-like language with arrays, records, and
pointers. We assign this language both a high-level semantics, where record
fields are accessed by name, and a low-level semantics, based on low-level
pointers. Ultimately, transformations could be defined as type-directed
source-to-source translations. For the moment, to simplify the proof, we
describe them as relations, and prove a forward simulation result. The talk
will give a tour of the language, the formalization of the transformations,
and the theorems proved.