会话类型

会话类型是一套用于描述通信协议的形式化类型系统，能够刻画先发后收、选择分支、递归等交互结构，并对通信双方的行为施加对偶约束。

学术界通常通过限制协议形式（如禁止在分支中改变角色集合、限制广播仅用于静态已知角色）来保证投影总是可判定的。