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