Logical semantics of types for concurrency

We motivate and present a logical semantic approach to types for concurrency and to soundness of related systems. The approach is illustrated by the development of a generic type system for the pi-calculus, which may be instantiated for specific notions of typing by extension with adequate subtyping principles. Soundness of our type system is established using a logical predicate technique, based on a compositional spatial logic interpretation of types.