铁氧体：Rust中会话类型的判断性嵌入
Ferrite: A Judgmental Embedding of Session Types in Rust
摘要：
本文介绍了Ferrite，它是Rust中会话类型的浅嵌入。与主流语言的现有会话类型库和嵌入相比，Ferrite不仅支持线性会话类型，还支持共享会话类型。共享会话类型允许共享（别名）通道，同时使用获取和释放会话的类型模态来保留会话保真度（保留）。Ferrite采用命题作为类型的方法，并将类型派生编码为Rust函数，并将成功的类型检查证明表现为Rust程序。我们使用Servo作为一个实际的例子来评估Ferrite，并演示如何使用Ferrite在画布组件中实现安全通信。
英文摘要：
This paper introduces Ferrite, a shallow embedding of session types in Rust. In contrast to existing session type libraries and embeddings for mainstream languages, Ferrite not only supports linear session types but also shared session types. Shared session types allow sharing (aliasing) of channels while preserving session fidelity (preservation) using type modalities for acquiring and releasing sessions. Ferrite adopts a propositions as types approach and encodes typing derivations as Rust functions, with the proof of successful type-checking manifesting as a Rust program. We provide an evaluation of Ferrite using Servo as a practical example, and demonstrate how safe communication can be achieved in the canvas component using Ferrite.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
