A Retargetable Polymorphic Type System for Mobility Calculi

移动性演算（如π演算和环境演算）对具有多台计算机和动态改变其连接和/或位置的程序的系统的行为进行数学建模。这些演算可以描述现有的系统或表达新的系统设计，并可以支持自动分析。有许多已知的迁移演算，并且每年都有许多新的演算被设计出来。类型是一个基本的计算机科学工具，用于确保程序和系统的安全性、正确性和安全性。类型对于组织编译、优化、代码生成和执行也很有用。由于这些和其他原因，移动性结石通常配备类型系统。然而，每一个新的演算都需要有一个专门为它设计的新的类型系统，这是一个繁琐的过程，类型系统的强度受到设计者已知的方法以及将每个方法设计成新的类型系统所需的时间和精力的限制。我们的项目将开发一个可重定向的类型系统，从该类型系统可以自动导出迁移演算的类型系统。这将使实验新的微积分变式更容易，从而使研究界能够更有效地发现哪些微积分在实践中有用。它还将支持在演算之间转移类型系统方法。与大多数现有的移动演算类型系统不同，我们的将支持多态性和主体类型。多态性对于泛型编程至关重要，因为在泛型编程中，单个系统部件必须处理许多数据类型。这对于现实世界的通信系统来说尤其重要，因为路由器或通信链路必须移动多种类型的数据，即使只有一种类型的数据。组合类型推断需要主类型，其中对系统片段的分析仅使用其子片段的分析结果，这些子片段可以以任何顺序独立分析。组合分析对于移动性非常重要，因为系统代码无法一次性用于静态分析。项目的起点是可重定向类型系统Poly*，我们已经将其开发到概念验证阶段，适用于许多移动性演算。我们在Poly* 上的工作证明了可重定向多态类型系统的想法是可行的，但是要使其足够通用以广泛使用还有很多工作要做。为了完成这项工作，我们提出了一个为期36个月的EPSRC项目，79个人月的工作量（包括PI），以及255 K的资金来支付合作研究者的工资，项目博士学位。奖学金及相关费用。

Mobility calculi such as the pi-calculus and ambient calculi mathematically model the behavior of systems with multiple computers and programs that dynamically change their connections and/or location. These calculi can describe existing systems or express new system designs, and can support automatic analysis. Numerous mobility calculi are known, and many new ones are designed each year.Types are a fundamental computer science tool for ensuring safety, correctness, and security of programs and systems. Types are also useful for organizing compilation, optimization, code generation, and execution. For these and other reasons, mobility calculi are usually equipped with type systems. However, each new calculus needs to have a new type system designed specifically for it. That is a tedious process and the type system's strength is limited by the methods known to its designers and the time and effort needed to design each method into a new type system.Our project will develop a retargetable type system from which type systems can be automatically derived for mobility calculi. This will make it easier to experiment with new calculus variations and thus enable the research community to more efficiently discover which calculi are useful in practice. It will also support transferring type system methods between calculi.Unlike most existing mobility calculi type systems, ours will support polymorphism and also principal typings. Polymorphism is vital for generic programming, where a single system part must handle many data types. This is particularly relevant for real-world communicating systems, where a router or a communication link must move many kinds of data even though there is only one of it. Principal typings are needed for compositional type inference, where the analysis for a system fragment uses only the analysis results for its subfragments, which can be analysed independently in any order. Compositional analysis is important for mobility, where a system's code will not be available for static analysis at a single time.The starting point for the project is the retargetable type system Poly* which we have already developed to a proof-of-concept stage where it works for many mobility calculi. Our work on Poly* demonstrates the idea of a retargetable polymorphic type system is viable, but there is much to be done to make it general enough to be widely useful. To do this work, we propose an EPSRC project for a duration of 36 months, effort of 79 person-months (including the PI), and funding of 255K to cover the co-investigator's salary, a project Ph.D. studentship, and related expenses.