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, bâtiment C

                            Lundi 10 avril, 10h30

                               ----------------
                               François Pottier
                               ----------------

                                 Inria Paris

             ====================================================
             Temporary Read-Only Permissions for Separation Logic
               (Making Separation Logic's Small Axioms Smaller)
             ====================================================

I will present an extension of Separation Logic with a general mechanism for
temporarily converting an arbitrary assertion P to a read-only form RO(P).
Whereas the points-to assertion x ~> 5 represents unique read-write access to
the memory cell at address x, whose current content is the value 5, its
read-only form RO(x ~> 5) represents shared read-only access to this cell,
and also guarantees that its current content is 5. A modified version of the
frame rule allows read-only assertions to appear within a lexical scope.

In circumstances where mutable data structures are temporarily accessed for
reading, read-only assertions enable more concise specifications and proofs
than full (read-write) assertions. They are less powerful than CSL's
fractional permissions or Rust's read-only borrows, but they are simpler.
Neither fractions nor lifetimes are required: read-only assertions can be
freely duplicated and discarded. The metatheory of read-only assertions is
very simple, too, and has been verified in Coq.

This is joint work with Arthur Charguéraud.