一句话：提出带消息观察会话类型的进程语言 Most，并基于带绑定的迹语义证明类型可靠性与组合性。
二元会话类型只能刻画局部通信协议，难以表达依赖其他通道消息的全局不变式。本文提出进程语言 Most，其消息观察式会话类型在二元会话类型上引入类型级计算，使协议能根据在其他通道上观察到的消息而变化，从而以自底向上、组合式的方式表达全局不变式。作者基于带绑定的迹（traces with binding）给出 Most 的语义基础，用于在存在名字生成时组合式地推理迹。基于该语义，证明了 Most 进程的类型可靠性与组合性。该工作向刻画消息依赖、提供更精确的进程保证迈出重要一步。
We present Most, a process language with message-observing session types. Message-observing session types extend binary session types with type-level computation to specify communication protocols that vary based on messages observed on other channels. Hence, Most allows us to express global invariants about processes, rather than just local invariants, in a bottom-up, compositional way. We give Most a semantic foundation using traces with binding, a semantic approach for compositionally reasoning about traces in the presence of name generation. We use this semantics to prove type soundness and compositionality for Most processes. We see this as a significant step towards capturing message-dependencies and providing more precise guarantees about processes.