The type discipline of behavioral separation

Research output: Contribution to journalConference articlepeer-review

5 Citations (Scopus)

Abstract

We introduce the concept of behavioral separation as a general principle for disciplining interference in higher-order imperative concurrent programs, and present a type-based approach that systematically develops the concept in the context of an ML-like language extended with concurrency and synchronization primitives. Behavioral separation builds on notions originally introduced for behavioral type systems and separation logics, but shifts the focus from the separation of static program state properties towards the separation 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 flexibility. 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, behavioral borrowing, and invariant-based separation.

Original languageEnglish
Pages (from-to)275-286
Number of pages12
JournalAcm Sigplan Notices
Volume48
Issue number1
DOIs
Publication statusPublished - 1 Jan 2013

Keywords

  • Behavioral types
  • Concurrency
  • Higher order programming
  • Interference
  • Separation

Fingerprint

Dive into the research topics of 'The type discipline of behavioral separation'. Together they form a unique fingerprint.

Cite this