Ownership types and Separation Logic seem to have similar goals, control over ownership and aliasing.  Perhaps, I should also add: the ability to write modular specifications.What is known about the relationship between ownership types and Separation Logic?
Ownership types and Separation Logic
pl.programming languages;type systems;object oriented;program logic
I recently finished writing a survey of Ownership Types and found very little that discusses the relationship between the two topics. The three closest papers I came across are the following, which curiously come from the same conference:Yang Zhao and John Boyland. A fundamental permission interpretation for ownership types. In Second IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, June 17-19, 2008, Nanjing, China. IEEE Computer Society, 2008., pages 6572. Shuling Wang, Lus Soares Barbosa, and Jos Nuno Oliveira. A relational model for confined separation logic. In In Second IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, June 17-19, 2008, Nanjing, China. IEEE Computer Society, 2008., pages 263270.Shuling Wang and Zongyan Qiu. A generic model for confinement and its application. In In Second IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, June 17-19, 2008, Nanjing, China. IEEE Computer Society, 2008., pages 5764.The first paper encodes two styles of ownership types, namely owners-as-dominators and owners-as-locks, in terms of Boyland's fractional permissions, which are a capability system developed for reasoning about programs. The second paper takes confinement ideas similar to those used in ownership types and adds them to separation logic. The third paper has developed a semantic approach which is used to encode various confinement disciplines such as ownership types. I'm not sure whether their system covers separation logic as well, and I cannot access it at the moment. Their approach is rather ad hoc; it can be seen as a more formal and systematic to a paper I wrote a while ago with James Noble and others:Towards a model of encapsulationJames Noble, Robert Biddle, Ewan Tempero, Alex Potanin, Dave ClarkeThe First International Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming (IWACO), 2003.