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.
翻译:本文介绍Ferrite, 这是在Rust 中浅浅嵌入的届会类型。 与现有的届会类型图书馆和主流语言嵌入不同, Ferrite 不仅支持线性届会类型,而且支持共享会话类型。 共享会话类型允许使用获取和释放会话的类型方式共享( 别名),同时保持会话的忠实性( 保全性) 。 Ferrite 采用一种建议作为类型方法,并将打字的衍生编码作为Rust 函数, 并证明成功进行类型检查是一个Rust 程序。 我们用Servo作为实例对 Ferrite 进行了评估, 并演示如何使用Ferrite 在画组组件中实现安全通信。