唯一性是分离
Uniqueness is Separation
AI总结：
本文提出通过分离逻辑断言表达值独立性，以解决唯一性类型系统在现实软件中的限制问题。
摘要：
在大规模软件系统推理中，值独立性带来巨大好处。这些好处也适用于形式验证领域。在证明助手中，用代数方法推理程序很简单，而具有无约束突变的程序则需要更复杂的技巧，如分离逻辑，其中必须通过手动证明建立关于内存安全、别名和状态变化的不变式。唯一性类型系统允许程序编译为使用突变提高效率的代码，同时保留具有值独立性的语义。然而，这些类型系统的限制往往对现实软件来说过于苛刻。因此，大多数唯一性类型系统包含某种“逃生口”，其中值独立性的好处被丧失，但唯一性类型的限制被解除。为了正式验证具有此类混合保证的系统，必须将值独立性保证用指令式、可变语义表达。换句话说，我们应当将值独立性作为分离逻辑中的断言来表达。
英文摘要：
Value independence is enormously beneficial for reasoning about software systems at scale. These benefits carry over into the world of formal verification. Reasoning about programs algebraically is a simple affair in a proof assistant, whereas programs with unconstrained mutation necessitate much more complex techniques, such as Separation Logic, where invariants about memory safety, aliasing, and state changes must be established by manual proof. Uniqueness type systems allow programs to be compiled to code that uses mutation for efficiency, while retaining a semantics that enjoys value independence for reasoning. The restrictions of these type systems, however, are often too onerous for realistic software. Thus, most uniqueness type systems include some "escape hatch" where the benefits of value independence for reasoning are lost, but the restrictions of uniqueness types are lifted. To formally verify a system with such mixed guarantees, the value independence guarantees from uniqueness types must be expressed in terms of imperative, mutable semantics. In other words, we ought to express value independence as an assertion in Separation Logic.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
