论文标题
π与剩菜：AGDA中的机械化
π with leftovers: a mechanisation in Agda
论文作者
论文摘要
线性类型系统需要跟踪程序如何使用其资源。标准方法是使用上下文拆分，指定资源的跨越跨越（不连贯）分裂。在这种方法中，上下文将划分的回声信息划分，该信息已经存在于复的信息中。另一种方法是使用剩余的键入，除了通常的（输入）用法上下文之外，键入判断还具有输出用法上下文：剩余的。在这种方法中，一个打字派生的剩余剩余作为输入输入到下一个，在避免上下文拆分的同时，通过线性资源进行螺纹。我们使用剩余键入来定义用于资源感知π-calculus的类型系统，这是用于建模并发系统的过程代数。我们的类型系统是在一组使用代数的参数上进行的，这些代数足以包含共享类型（免费重复使用和丢弃），分级类型（精确使用n次次数）和线性类型（精确使用一次）。线性类型在π级别中很重要：它们确保了沟通的隐私和安全性并避免种族条件，而分级和共享类型则可以进行更灵活的编程。我们为我们的类型系统提供了框架定理，将弱化的定理概括为包括线性类型，并证明受试者还原。我们的形式化已在约1850条AGDA线上完全机械化。
Linear type systems need to keep track of how programs use their resources. The standard approach is to use context splits specifying how resources are (disjointly) split across subterms. In this approach, context splits redundantly echo information which is already present within subterms. An alternative approach is to use leftover typing, where in addition to the usual (input) usage context, typing judgments have also an output usage context: the leftovers. In this approach, the leftovers of one typing derivation are fed as input to the next, threading through linear resources while avoiding context splits. We use leftover typing to define a type system for a resource-aware π-calculus, a process algebra used to model concurrent systems. Our type system is parametrised over a set of usage algebras that are general enough to encompass shared types (free to reuse and discard), graded types (use exactly n number of times) and linear types (use exactly once). Linear types are important in the π-calculus: they ensure privacy and safety of communication and avoid race conditions, while graded and shared types allow for more flexible programming. We provide a framing theorem for our type system, generalise the weakening and strengthening theorems to include linear types, and prove subject reduction. Our formalisation is fully mechanised in about 1850 lines of Agda.
