Wei Zhang (张蔚)

共同作者 (with Yifan Shi and Tianyi Cui)，Shi Zhang & Cui 2026 A Programming Paradigm for Spatiotemporal Composability。北京大学（PKU）affiliation。

关键贡献

Revertible Effects 形式化——effect context \partial\Gamma := \Gamma \times (\Gamma \to \Gamma)；track 操作的单调同态性（Theorem 5）；累加器 LIFO 撤销的 soundness invariant（Theorem 7）。
Reactive Coeffects 形式化——specification d、notification 三态、isolation realm、interception metadata；Theorem 42 把"键上操作可交换"作为独立性条件。
Calculus 形式化（与 Yifan Shi 合作）——component、fiber、registry、target view；O-Insert / O-Retire / O-Remove / L-Reload / L-Unload 五条 base 规则；L-Leave + relied 守卫；Theorem 63（coeffect 排序）与 Theorem 66（guard release）解决"被卸载者所有依赖者完成 teardown 才撤销"问题。
Metatheory——preservation、progress、confluence（Theorem 65：调度无关性）、quiescent state function of final config（Theorem 73）。