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 - Rocquencourt
                         Amphi Turing du bâtiment 1

                              Lundi 17 mars, 14h

                               ----------------
                               Sigurd Schneider
                               ----------------

                         Universität des Saarlandes

         ============================================================
         Translating In and Out of a Functional Intermediate Language
         ============================================================

                   [PLEASE NOTE THE UNUSUAL TIME: 14:00]

To use a functional intermediate language for the compilation of an
imperative language two translations are of particular importance:
Translating from the imperative source language (e.g. C) into the
functional language, and translating out of the functional language
to an imperative target language (e.g. assembly).

This talk discusses the above translations in the context of the
intermediate language IL.  IL comes with an imperative and a
functional interpretation.  IL/I (imperative interpretation) is a
register transfer language close to assembly.  IL/F (functional
interpretation) is a first-order functional language with a tail-call
restriction.  We devise the decidable notion of coherence to identify
programs on which the semantics of IL/I and IL/F coincide.
Translations between the interpretations are obtained from
equivalence-preserving translations to the coherent fragment.  The
translation from IL/I to IL/F corresponds to SSA construction.  The
translation from IL/F to IL/I can be seen as register assignment.

The translations are formalized and proven correct using the proof
assistant Coq.  Extraction yields translation-validated
implementations of SSA construction and register assignment from the
above translations.