Citation:

Caires, L, Seco JC.  2013.  The Type Discipline of Behavioral Separation. Proceedings of the 40th Symposium on Principles of Programming Languages (POPL).

Abstract:

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.

Notes:

to appear

Related External Link