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

                         VENDREDI 21 octobre, 10h30

                               -------------
                               Peter O'Hearn
                               -------------

                      Queen Mary University of London

                   =====================================
                   Algebra, Logic, Locality, Concurrency
                   =====================================

This talk reports on ongoing work -- with Tony Hoare, Akbar Hussain, Bernhard
Moller, Rasmus Petersen, Georg Struth, Ian Wehrman, and others -- on models
and logics for concurrent processes.

The approach we are taking abstracts from syntax or particular models.
Message passing and shared memory process interaction, and strong
(interleaving) and weak (partial order) approaches to sequencing, are
accomodated as different models of the same core axioms. Rules of program
logic, related to Hoare and Separation logics, flow at once from the algebraic
axioms. So, one gets a generic program logic from the algebra, which holds
for a range of concrete models.