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 4 février, 10h30

                              ---------------
                              Robert Krebbers
                              ---------------

                        Radboud University Nijmegen

   =====================================================================
   Separation Logic for Non-local Control Flow and Block Scope Variables
   =====================================================================

We present an approach for handling non-local control flow (goto and return
statements) in the presence of allocation and deallocation of block scope
variables in imperative programming languages.

We define a small step operational semantics and an axiomatic semantics (in
the form of a separation logic) for a small C-like language that combines
these two features, and which also supports pointers to block scope
variables. Our operational semantics represents the program state through a
generalization of Huet's zipper data structure.

We prove soundness of our axiomatic semantics with respect to our operational
semantics. This proof has been fully formalized in Coq.