Publications

Export 4 results:
Sort by: [ Author  (Asc)] Title Type Year
A B [C] D E F G H I J K L M N O P Q R S T U V W X Y Z   [Show ALL]
C
Caires, L, Ferreira C, Ravara A.  2010.  A simple proof system for lock-free concurrency. International Workshop on Proof Systems for Program Logics (PSPL). Abstract
n/a
Caires, L, Seco JC.  2012.  The Type Discipline of Behavioral Separation (Long version with proofs). : CITI / DI-FCT-UNL Abstract
n/a
Caires, L, Seco JC.  2012.  Working note on a type-checking algorithm for BST. : CITI / DI-FCT-UNL Abstract
n/a
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.