MEBI: Mechanised Bisimilarities and Behavioural-typed Processes

构建正确的通信系统(即并发和分布式系统)是一项艰巨的任务。这类系统往往呈现出难以重现的非确定性行为。这意味着，每当这类系统中的一个系统出现错误时，修复它就是一项既耗时又昂贵的任务。此外，分布式系统目前在我们的社会中非常普遍，包括银行或电子医疗等关键行业。因此，通信系统中的漏洞可能会造成很大的破坏，威胁到巨大的经济成本，以及依赖它们的行业的安全和保障。为了确保通信系统的正确性，已经开发了许多工具和理论。会话类型是验证通信系统中是否存在并发错误的最有影响力的理论之一。会话类型可以保证流程实现只遵循指定的结构化操作序列(发送/接收)。这些规范有效地代表了通信协议，会话类型理论提供了验证它们不存在并发错误的技术。会话类型最有影响力的扩展之一是多方会话类型理论(MPST)，它允许在任意数量的参与者之间对协议进行建模，并已与许多主流语言集成在一起。然而，大多数基于会话类型的工具并不遵循科学出版物中提出的确切理论，因为它们还需要考虑工程问题。此外，大多数会话类型的理论都被复杂的纸笔证明是正确的。这样的证明可能包含错误，文献中展示了这些情况的例子。这是对大量工作有效性的一大威胁。证明助手是可以保证这些合理论点的正确性的工具。在证明助手中编码语言、工具和理论称为机械化，它导致了计算机科学中有很大影响的发展，例如CompCert，一个经过认证的C编译器，它被证明比其他同类编译器产生的错误要少得多，目前正被用于关键系统的上下文中。但是证明机械化是非常困难的，在机械化MPST方面没有太多的工作。MPST机械化的主要障碍之一是进程等价性或生物相似性的概念。根据标记的状态转换系统(LTS)语义，非正式地，如果两个进程相互匹配，则它们是双相似的。证明生物相似性的一种主要技术被称为互模拟证明方法，它依赖于找到两个进程之间的关系，以保证它们将根据它们的LTS匹配彼此的动作。这些证明在并发理论中很普遍，也是MPST机制成功的关键。我们需要一种方法来简化LTS语义和生物相似性证明的机械化。我们将研究常见的互模拟证明技术和算法，并找到并实现适合机械化的候选方法。我们的主要目标是尽可能地自动化LTS语义的机械化。关键的挑战之一是找到合适的定义：纸笔校样往往会忽略机械化过程中重要的细节。例如，终止通常在纸笔证明中是非正式的，但具体细节是成功机械化的关键。我们将在Coq证明助手中机械化LTS语义和生物相似性的通用框架，并在项目合作伙伴的两个案例研究中使用它。这些案例研究将既是评估成功的一种方式，也是该项目的主要推动因素。最后，我们将在我们的框架内研究认证实现的提取，从而有助于提高分布式系统的安全性和可靠性。

Building correct communicating systems (i.e. concurrent and distributed systems) is a hard task. Such systems often present non-deterministic behaviours that are hard to reproduce. This means that, whenever there is a bug in one of such systems, fixing it is a time consuming and costly task. Furthermore, distributed systems are nowadays widespread in our society, including key sectors such as banking or E-healthcare. Thus, bugs in communicating systems can be very damaging, threatening large economic costs, and the safety and security of the industries that rely on them.To guarantee the correctness of communicating systems, many tools and theories have been developed. Session types are among the most influential theories for verifying the absence of concurrency bugs in communicating systems. Session types can guarantee that process implementations only follow the specified structured sequence of actions (send/receive). These specifications effectively represent communication protocols, and session type theories provide techniques to verify that they are absent of concurrency bugs. Among the most influential extensions of session types is the theory of Multiparty Session Types (MPST), which enables the modelling of protocols among an arbitrary number of participants, and has been integrated with many mainstream languages.However, most of the tools based on session types are not following the exact theories that are presented in the scientific publications, since they also need to take into account engineering issues. Furthermore, most of the session type theories are proven correct using complex pen-and-paper soundness proofs. Such proofs can contain errors, and the literature shows examples of these cases. This is a big threat to the validity of large bodies of work. Proof assistants are tools that can guarantee the correctness of these soundness arguments. Encoding languages, tools, and theories in a proof assistant is called mechanisation, and it has led to large influential developments in computer science, such as CompCert, a certified C compiler that has proven to present significantly less bugs than other comparable compilers, and that is currently being used in the context of critical systems.But proof mechanisation is significantly hard, and not much work exists on mechanising MPST. One of the main hurdles in mechanising MPST is the notion of process equivalence, or bisimilarity. Informally, two processes are bisimilar if they match each others actions, according to their Labelled-state Transition System (LTS) semantics. One main techniques for proving bisimilarity is known as the bisimulation proof method, which relies on finding a relation between two processes that guarantees that they will match each other's moves according to their LTS. These proofs are widespread in concurrency theory, and are key to successful mechanisations of MPST. We need a way to simplify the mechanisation of LTS semantics, and bisimilarity proofs.We will study common bisimulation proof techniques and algorithms, and find and implement a suitable candidate for mechanisation. Our main goal is to automate as much as possible of the mechanisation of the LTS semantics. One of the key challenges is to find the suitable definitions: pen-and-paper proofs can often overlook details that are important in a mechanisation. For example, termination is often informally justified in pen-and-paper proofs, but the specific details are key to a successful mechanisation. We will mechanise a generic framework for LTS semantics and bisimilarity in the Coq proof assistant, and use it in two case studies from the project partners. These case studies will serve both as a way to evaluate success, and as main driving elements of this project. Finally, we will study the extraction of certified implementations within our framework, thus contributing to increase the safety and reliability of distributed systems.