Formal verification methods for concurrent systems cannot always be scaled-down or tailored in order to be applied on specific subsystems. We address such an issue in a MultiParty Session Types setting by devising a partial type assignment system for multiparty sessions (i.e. sets of concurrent participants) with asynchronous communications. Sessions are possibly typed by "asynchronous global types" describing the overall behaviour of specific subsets of participants only (from which the word "partial"). Typability is proven to ensure that sessions enjoy the partial versions of the well-known properties of lock- and orphan-message-freedom.

翻译：并发系统的形式化验证方法往往难以按比例缩减或定制以应用于特定子系统。针对这一问题，我们在异步通信的多方会话（即并发参与者集合）环境中，设计了一种部分类型分配系统。会话可由"异步全局类型"进行类型标注，该类型仅描述特定参与者子集的整体行为（"部分"一词即源于此）。研究证明，类型可分配性能够确保会话满足无锁消息与无孤儿消息这两类经典性质的部分版本。