Logical Semantics of Types for Concurrency

We motivate and present a logical semantic approach to types for concurrency and to the 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.

• Type: Conference
• Year: 2007
• Where: CALCO
• Authors: Luís Caires
• Keywords: Adequate Subtyping Principles, CALCO 2007, Logical Predicate Technique, Logical Semantic Approach