A filter model for mobile processes This work was partly supported by NATO Grant HTECH. LG960875.

摘要: This paper presents a filter model for π-calculus and shows its full abstraction with respect to a ‘may’operational semantics. The model is introduced in the form of a type assignment system. Types are related by a preorder that mimics the operational behaviour of terms. A subject expansion theorem holds. Terms are interpreted as filters of types: this interpretation is compositional. The proof of full abstraction relies on a notion of realizability of types and on the construction of terms, which test when an arbitrary term has a fixed type.