CITI has stopped operations in 2014, to co-launch NOVA LINCS THIS SITE IS NOT BEING UPDATED SINCE 2013
citi banner
Home Page FCT/UNL UNL
  Home  \  Seminars @ CITI  \  Seminar Page Login  
   
banner bottom
File Top
The Type Discipline of Behavioral Separation
{ Tue, 18 Jun 2013, 14h00 }

By: Luis Caires

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.

Luís Caires (joint work with João C. Seco)


Hosted by: Software Systems

Location: DI seminars room

File Bottom