An Asynchronous Soundness Theorem for Concurrent Separation Logic. Concurrent separation logic (CSL) is a specification logic for concurrent imperative programs with shared memory and locks. We develop a concurrent and interactive account of the logic inspired by asynchronous game semantics. To every program C, we associate a pair of asynchronous transition systems ⟦C⟧S and ⟦C⟧L which describe the operational behavior of the Code when confronted to its Environment (or Frame) – both at the level of machine states (S) and of machine instructions and locks (L). We then establish that every derivation tree π of a judgment Γ⊢{P}C{Q} defines a winning and asynchronous strategy ⟦π⟧Sep with respect to both asynchronous semantics ⟦C⟧S and ⟦C⟧L. From this, we deduce an asynchronous soundness theorem for CSL, which states that the canonical map ℒ:⟦C⟧S→⟦C⟧L, from the stateful semantics ⟦C⟧S to the stateless semantics ⟦C⟧L satisfies a basic fibrational property. We advocate that this provides a clean and conceptual explanation for the usual soundness theorem of CSL, including the absence of data races. This is joint work with Paul-André Melliès. Organization of the talk: In a first part, I will give a high level view of our semantics and of the soundness theorem, essentially as it appeared in our previous paper. In a second part, I will talk in more details about our new semantics of CSL, which has a more algebraic flavor (work in progress).