Publications

Export 6 results:
Sort by: Author Title Type [ Year  (Desc)]
2013
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.

2012
Caires, L, Seco JC.  2012.  The Type Discipline of Behavioral Separation (Long version with proofs). : CITI / DI-FCT-UNL Abstract
n/a
Baltazar, P, Caires L, Vasconcelos VT, Vieira HT.  2012.  A Type System for Flexible Role Assignment in Multiparty Communicating Systems. Proceedings of the 7th International Symposium on Trustworthy Global Computing (TGC). Abstract
n/a
Caires, L, Seco JC.  2012.  Working note on a type-checking algorithm for BST. : CITI / DI-FCT-UNL Abstract
n/a
2010
Militão, F, Aldrich J, Caires L.  2010.  Aliasing control with view-based typestate. Formal Techniques for Java Programs (FTfJP). Abstract
n/a
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