paperbot · PL 论文追踪

全部论文 待读 收藏

P2 RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly

RichWasm：将安全、细粒度、共享内存互操作性下沉至 WebAssembly
PLDI 8(PLDI)2024匹配度 2/10 · 论文属于编程语言类型系统与编译领域的形式化验证工作，未涉及 LLM/Agent，也不涉及静态分析、浮点或贝叶斯程序分析，与用户关注的核心交叉方向（PL与AI结合）不匹配。引用 5 inbox
Michael Fitzgibbons, Zoe Paraskevopoulou, Noble Mushtak, Michelle Thalakottur, Jose Sulaiman Manzur, Amal Ahmed
类型系统编译与代码生成定理证明与证明工程
dblp: 2026-09-10crossref: 2026-09-10arxiv: 2026-09-10

AI 速览

一句话：提出 RichWasm，一种支持安全共享内存互操作并可编译到 WebAssembly 的富类型中间语言，并在 Coq 中证明类型安全。

不同语言具有不同内存安全保证，跨语言共享内存互操作可能破坏内存安全。本文提出 RichWasm：一种基于 WebAssembly 的富类型中间语言，用作带类型的高级语言编译目标。它通过细粒度内存所有权与共享等类型特性，支持垃圾回收语言与基于所有权、手动内存管理语言之间的安全共享内存互操作。作者给出从 core ML 和带强更新的类型安全语言 L3 到 RichWasm 的编译器，并将 RichWasm 编译到普通 Wasm 以复用现有环境。RichWasm 已在 Coq 中形式化，并证明了类型安全性。

问题
跨语言共享内存互操作时，不同语言类型系统与内存安全保证不同，容易在边界处引发内存安全违规；现有 Wasm 缺乏表达细粒度所有权与共享的类型设施，难以作为异构有类型语言的统一编译目标。
方法
提出 RichWasm，一种基于 WebAssembly 的富类型中间语言，引入支持细粒度内存所有权和共享的类型特性；给出从 core ML 与 L3 到 RichWasm 的编译器，并将 RichWasm 编译到普通 Wasm，同时在 Coq 中形式化其类型系统。
评估
通过为 core ML 和 L3 实现到 RichWasm 的编译器并编译回普通 Wasm 来展示可行性，并在 Coq 中机器化证明 RichWasm 的类型安全性。
原文摘要（Abstract）

Safe, shared-memory interoperability between languageswith different type systems and memory-safety guarantees is an intricate problem as crossing language boundaries may result in memory-safety violations. In this paper, we present RichWasm, a novel richly typed intermediate language designed to serve as a compilation target for typed high-level languages with different memory-safety guarantees. RichWasm is based on WebAssemblyand enables safe shared-memory interoperability by incorporating a variety of type features that support fine-grained memory ownership and sharing. RichWasm is rich enough to serve as a typed compilation target for both typed garbage-collected languages and languages with an ownership-based type system and manually managed memory. We demonstrate this by providing compilers from core ML and L 3 , a type-safe language with strong updates, to RichWasm. RichWasm is compiled to regular Wasm, allowing for use in existing environments. We formalize RichWasm in Coq and prove type safety.

链接与引用

DOI 原文 · arXiv · PDF（开放获取） · DBLP

BibTeX 
@article{FitzgibbonsPMTMA24,
  title = {RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly},
  author = {Michael Fitzgibbons and Zoe Paraskevopoulou and Noble Mushtak and Michelle Thalakottur and Jose Sulaiman Manzur and Amal Ahmed},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {PLDI},
  year = {2024},
  doi = {10.1145/3656444}
}