Message-Observing Sessions
Proceedings of the ACM on Programming Languages(2024)
摘要
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.
更多查看译文
关键词
dependent types,program specification,session types,trace semantics
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要