Wei Zhang (张蔚)

大白话：北京大学的研究者，研究编程语言的形式化方法，与 Yifan Shi、Tianyi Cui 合作提出时空可组合性（spatiotemporal composability）的编程范式。

Shi Zhang & Cui 2026 A Programming Paradigm for Spatiotemporal Composability 的共同作者。所属机构：北京大学（PKU）。

关键贡献

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）。