–
Room P3.10, Mathematics Building
Luís Caires, CITI, U Nova de Lisboa
Space-time types for concurrency control
We develop a notion of spatial-behavioral typing particularly suitable to discipline interactions and resource usage in concurrent programs. Our type structure reflects a resource aware model of behavior, where a parallel composition type operator expresses resource independence, a sequential composition type operator expresses implicit synchronization, and a modal type operator expresses resource ownership. Soundness of our type system is established using a logical relations technique, building on a interpretation of types as properties expressible in a spatial logic.