This talk explores the relation between two formalisms and one algebraic framework for concurrency. Session Types and Concurrent Separation Logic are formalisms that support independent reasoning about concurrent processes. We first translate a small language we call Baby Session Types (BST), into a “basic” version of Concurrent Separation Logic (BCSL), and we show that the translation is sound and complete. We then describe a model for BCSL (hence, BST), which exhibits an algebraic structure of two semigroups (for sequential and parallel composition) linked by an exchange law as advanced recently in Concurrent Kleene Algebra. The model construction is very general, starting from any partial commutative monoid of propositions. However, an instantiation where Session Type contexts are the propositions provides a natural model of and concrete meaning to a notion of Hoare triples in the algebra models, corresponding to the intuition of a typing (assertion) as providing an over-approximation of the future.