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 a lambda calculus extended with
mutable state, concurrency, and synchronizatin primatives.
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.
We illustrate how our type
system, even if based on a small set of fairly canocical primatives, is
already able to tackle challenging program idoms, involving alaising at
all types, concurrency with first-class threads, manipulation of linked
data structures, behavioral borrowing, and invariant-based separation.
Luis Caires (joint work with Joao C. Seco) based on work to be presented at POPL'13.