Luis Cairer
Universidade Nova, Lisbon, Portugal

Challenges and Progress with Feature-Rich Data

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.


Host: Frank Pfenning

Friday, December 7, 2012
2:00 p.m.
Gates & Hillman Centers 7501

Principles of Programming Seminars