@conference {Popl,
	title = {The Type Discipline of Behavioral Separation},
	booktitle = {Proceedings of the 40th Symposium on Principles of Programming Languages (POPL)},
	year = {2013},
	note = {<p>to appear</p>
},
	abstract = {<p>We introduce the concept of behavioral separation as a general prin- ciple for disciplining interference in higher-order imperative con- current programs, and present a type-based approach that system- atically develops the concept in the context of an ML-like language extended with concurrency and synchronization primitives. Behav- ioral separation builds on notions originally introduced for behav- ioral type systems and separation logics, but shifts the focus from the separation of static program state properties towards the sep- aration of dynamic usage behaviors of runtime values. Behavioral separation types specify how values may be safely used by client code, and can enforce fine-grained interference control disciplines while preserving compositionality, information hiding, and flexi- bility. We illustrate how our type system, even if based on a small set of general primitives, is already able to tackle fairly challenging program idioms, involving aliasing at various types, concurrency with first-class threads, manipulation of linked data structures, be- havioral borrowing, and invariant-based separation.</p>
},
	url = {http://ctp.di.fct.unl.pt/~lcaires/papers/bst-TR.pdf},
	author = {Lu{\'\i}s Caires and Jo{\~a}o Costa Seco}
}
