Sessions are a fundamental notion in message-passing systems. A session is an abstract notion of communication between parties where each one owns an endpoint. Session types are types that are assigned to the endpoints and that are used to statically and dynamically enforce some desired properties of the communications, such as the absence of deadlocks. Properties of concurrent systems are usually divided in safety and liveness ones and depending on the class it belongs to, a property is defined using different (dual) techniques. However, there exist some properties that require to mix both techniques and the challenges in defining them are exacerbated in proof assistants (e.g. Agda, Coq, . . . ), that is, tools that allow users to formally characterize and prove theorems. In particular, we mechanize the meta-theory of inference systems in Agda. Among the interesting properties that can be studied in the session-based context, we study fair termination which is the property of those sessions that can always eventually reach successful termination under a fairness assumption. Fair termination implies many desirable and well known properties, such as lock freedom. Moreover, a lock free session does not imply that other sessions are lock free as well. On the other hand, if we consider a session and we assume that all the other ones are fairly terminating, we can conclude that the one under analysis is fairly terminating as well.

翻译：会话是消息传递系统中的基本概念。会话是各方之间通信的抽象概念，其中每一方都拥有一个端点。会话类型是分配给端点的类型，用于静态和动态地强制实现通信的某些期望属性，例如无死锁。并发系统的属性通常分为安全性和活性两大类，根据其所属类别，属性使用不同（对偶）技术来定义。然而，有些属性需要混合使用这两种技术，而在证明助手（例如Agda、Coq等）中定义这些属性的挑战更为严峻，这些工具允许用户正式描述并证明定理。具体而言，我们在Agda中机械化推理系统的元理论。在基于会话的上下文中可研究的众多有趣属性中，我们特别研究公平终止，即在公平性假设下会话总能最终成功终止的属性。公平终止蕴含许多理想且众所周知的属性，例如无锁性。此外，无锁会话并不意味着其他会话也无锁。另一方面，如果考虑一个会话并假设所有其他会话都公平终止，则可以得出结论：当前分析的会话也公平终止。