带有借用机制的 Typestate 的法律与秩序
Law and Order for Typestate with Borrowing
AI总结：
提出一种基于有序类型和束状蕴涵的、支持借用机制的 typestate 新基础，并证明其类型健全性，实现了类型检查器和解释器。
摘要：
Typestate 系统众所周知地复杂，因为它们需要复杂的机制来跟踪别名。我们在非纯函数式编程的背景下，提出了一种新的、面向转换的 typestate 基础。我们的方法依赖于有序类型来进行简单的别名跟踪，其形式化借鉴了关于束状蕴涵（bunched implications）的工作。然而，我们在 typestate 存在的情况下支持灵活的借用概念。我们的核心演算包含一种资源类型的概念，该概念由一个有序部分幺半群索引，用于建模抽象状态转换。我们证明了相对于资源化仪表语义的语法类型健全性。我们给出了类型系统的算法版本并证明了其健全性。算法类型化促进了一种简单的表面语言，该语言不暴露有序类型的繁琐细节。我们为表面语言实现了一个类型检查器，并为核心语言实现了一个解释器。
英文摘要：
Typestate systems are notoriously complex as they require sophisticated machinery for tracking aliasing. We propose a new, transition-oriented foundation for typestate in the setting of impure functional programming. Our approach relies on ordered types for simple alias tracking and its formalization draws on work on bunched implications. Yet, we support a flexible notion of borrowing in the presence of typestate. Our core calculus comes with a notion of resource types indexed by an ordered partial monoid that models abstract state transitions. We prove syntactic type soundness with respect to a resource-instrumented semantics. We give an algorithmic version of our type system and prove its soundness. Algorithmic typing facilitates a simple surface language that does not expose tedious details of ordered types. We implemented a typechecker for the surface language along with an interpreter for the core language.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
