逃离自我：具有避免性的双向typing用于声音和表达式
Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types
AI总结：
本文提出了一种算法可达性类型，通过灵活的自我引用和双向类型算法，实现了在复杂对象图中安全跟踪可达性，避免了类型中的非法作用域名称。
摘要：
在存在突变和别名的情况下对程序进行推理非常困难。Rust通过生命周期为基础的所有权跟踪在系统编程中流行起来，但其“共享XOR可变”模型与更高层次的功能编程从根本上矛盾。可达性类型提供了一种替代方案：通过跟踪每个表达式结果可以到达的资源，使安全共享和逃逸可变数据成为可能。为了在复杂的对象图中跟踪内部可达性，可达性类型采用自我引用，使组件能够从内部引用封闭资源，就像面向对象语言中的this指针一样。虽然对于声明性地类型化逃逸数据是自然的，但自我引用会复杂化子类型和进一步的类型推断：方差限制了自我引用可能出现的位置，但有用的类型转换必须允许它们以受控的方式变化，这又对推断施加了约束。作为一种不受欢迎的结果，先前的工作要求程序员插入术语级的转换以仅仅避免非法作用域名称。由于所有先前的工作都是声明性的，我们在本文中研究了算法可达性类型。我们引入了一种更精细的子类型关系，使自我引用的使用更加灵活。我们进一步开发了一种安全且可决定的双向类型算法，该算法在Lean中实现并验证。该算法自动避免类型中的非法作用域名称，并通过轻量级的统一机制推断资格符。作为迈向实际可达性编程的一步，我们展示了该系统能够跟踪各种可达性模式，而无需在复杂Church编码数据类型中显式转换。
英文摘要：
Reasoning about programs in the presence of mutation and aliasing is notoriously difficult. Rust has popularized lifetime-based ownership tracking in systems programming, but its "shared XOR mutable" model is fundamentally at odds with higher-level functional programming. Reachability types offer an alternative: they enable safe sharing and escape of mutable data by tracking which resources each expression's result can reach. To track internal reachability within complex object graphs, reachability types adopt self-references that let components refer to enclosing resources from inside, just like `this` pointers in OO languages. While natural for declaratively typing escaping data, self-references complicate subtyping and furthermore type inference: variance restricts where self-references may appear, yet useful type conversions must allow them to vary in controlled ways, which in turn imposes constraints on inference. As an undesirable result, prior works require programmers to insert term-level coercions for even just avoidance -- avoiding ill-scoped names in types. With all prior works being declarative, we investigate algorithmic reachability types in this work. We introduce a refined subtyping relation that permits more flexible usages of self-references. We further develop a sound and decidable bidirectional typing algorithm, implemented and verified in Lean. The algorithm automatically avoids ill-scoped names in types, and infers qualifiers via a lightweight unification mechanism. As a step towards practical reachability programming, we show that the system is capable of tracking diverse reachability patterns without explicit coercions in complex Church-encoded datatypes.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
