一句话：在 Rocq 中机械化 WasmFX 并证明类型可靠性，提出 Iris 程序逻辑验证使用效应处理器的 Wasm 程序。
WasmFX 是在底层可移植字节码 Wasm 上增加以续延形式显式操作执行栈的扩展，并通过效应处理器接口支持非局部控制流的模块化编译。这类代码难以推理，其语言扩展的可靠性与手写库的正确性亟需验证。本文首先提出 WasmFXCert，在 Rocq 中机械化 WasmFX 并证明期望的类型可靠性；随后提出 Iris-WasmFX，一个用于推理使用效应处理器的 Wasm 程序的程序逻辑。作者将逻辑应用于两个关键用例：协程库和生成器。该工作验证了 WasmFX 的设计，并为未来基于效应的库提供模块化验证框架。
WasmFX is a proposed extension of Wasm, a low-level portable bytecode, with primitives for explicitly manipulating execution stacks as continuations. By exposing an interface of effect handlers, WasmFX enables non-local control flow features to be compiled in a modular way: one handcrafts a library that directly implements such features in WasmFX, and compilation then merely calls into the library. Alas, code involving non-local control flow is notoriously challenging, and so this proposal raises the questions of the soundness of the language extension, and of the correctness of such handcrafted libraries. In this paper, we first describe WasmFXCert, a mechanisation of WasmFX in Rocq, and prove the expected type soundness result. We then develop Iris-WasmFX, a program logic to reason about Wasm programs that use effect handlers, and illustrate its application to two key use cases of effect handlers: a coroutine library, and a generator. Together, these validate the design of WasmFX, and provide a modular framework for verifying future effect-based libraries.
@article{paperbot3762,
title = {Iris-WasmFX: Modular Reasoning for Wasm Stack Switching},
author = {Maxime Legoupil and Mathias Pedersen and Lars Birkedal and Sam Lindley and Jean Pichon-Pharabod},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808271}
}