Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct:
                  https://webconf.math.cnrs.fr/b/fra-ryy-fjn

			     S É M I N A I R E

                   ______                __    _
                  / ____/___ _____ ___  / /_  (_)_  ______ ___
                 / /   / __ `/ __ `__ \/ __ \/ / / / / __ `__ \
                / /___/ /_/ / / / / / / /_/ / / /_/ / / / / / /
                \____/\__,_/_/ /_/ /_/_.___/_/\__,_/_/ /_/ /_/

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

                           Lundi 25 octobre, 10h30

                                --------------
                                Léo Stefanesco
                                --------------

                                   MPI-SWS

 ===========================================================================
 Trillium: Unifying Refinement and Higher-Order Distributed Separation Logic
 ===========================================================================

We present a unification of refinement and Hoare-style reasoning in a
foundational mechanized higher-order distributed separation logic. This
unification enables us to prove in the Coq proof assistant that concrete
implementations of challenging distributed systems both refine more abstract
models and satisfy functional correctness properties using a single Hoare
triple. We use our logic to prove correctness of concrete implementations of
two-phase commit and single-decree Paxos by showing that they refine their
abstract TLA+ specifications. We further use our notion of refinement to
transfer fairness assumptions on program executions to model traces and then
transfer liveness properties of fair model traces back to program executions,
which enables us to prove liveness properties such as strong eventual
consistency of a concrete implementation of a Conflict-Free Replicated Data
Type and fair termination of a concurrent program.