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 Lions 1

                             MARDI 29 mars, 10h30

                              -----------------
                              Filip Sieczkowski
                              -----------------

                                    INRIA

       ================================================================
       Transfinite Step-indexing: Decoupling Concrete and Logical Steps
       ================================================================

Step-indexing has proven to be a powerful technique for defining logical
relations for languages with advanced type systems and models of expressive
program logics. In both cases, the model is stratified using natural numbers
to solve a recursive equation that has no naive solutions.  As a result of
this stratification, current models require that each unfolding of the
recursive equation – each logical step – must coincide with a concrete
reduction step. This tight coupling is problematic for applications where the
number of logical steps cannot be statically bounded.

We demonstrate that this tight coupling between logical and concrete steps is
artificial and show how to loosen it using transfinite step-indexing. We
present a logical relation that supports an arbitrary but finite number of
logical steps for each concrete step.