会话协奏曲：会话的公平终止

会话是消息传递系统中的基本概念。会话是参与方之间通信的抽象概念，其中每一方拥有一个端点。会话类型是被赋予端点的类型，用于静态和动态地强制实施通信的某些期望性质，例如无死锁。并发系统的性质通常分为安全性和活性两类，根据所属类别不同，性质使用不同（对偶）的技术来定义。然而，存在一些性质需要混合两种技术，且在证明辅助工具（如 Agda、Coq 等，即允许用户形式化刻画并证明定理的工具）中定义这些性质的挑战被加剧了。特别地，我们在 Agda 中机械化了推理系统的元理论。在基于会话的语境中可研究的诸多有趣性质里，我们研究公平终止，即在公平性假设下那些会话总能最终达到成功终止的性质。公平终止蕴含许多期望且熟知的性质，例如无锁性。此外，一个无锁的会话并不意味着其他会话也是无锁的。另一方面，若我们考虑一个会话并假设所有其他会话均公平终止，则可断定所分析的该会话也是公平终止的。