Spatial-behavioral types for concurrency and resource control in distributed systems

We develop a notion of spatial-behavioral typing suitable to discipline concurrent interactions and resource usage in distributed object systems. Our type structure reflects a resource sensitive model, where a parallel composition type operator expresses resource independence, a sequential composition type operator expresses resource synchronization, and a type modality expresses resource ownership. We model the intended computational systems using a concurrent object calculus. 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.

• Type: Journal
• Year: 2008
• Where: TCS
• Authors: Luís Caires
• Keywords: Composition Type Operator, Parallel Composition Type, Resource, TCS 2008, Theoretical Computer Science