  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.
