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π-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.
|Title of host publication||Lecture Notes in Computer Science|
|Publication status||Published - 1 Jan 2007|
|Event||Algebra and Coalgebra in Computer Science, Second International Conference, CALCO 2007 - |
Duration: 1 Jan 2007 → …
|Conference||Algebra and Coalgebra in Computer Science, Second International Conference, CALCO 2007|
|Period||1/01/07 → …|