ICSE 2291 ASE 2141 FSE 1566 ASPLOS 1219 LMCS 1020 OOPSLA 737 LICS 679 ISSTA 617 POPL 609 ICFP 374 PLDI 369 TOPLAS 199 JFP 172 arXiv 预印本 5
标签：形式语义（共 1150 篇，按优先级展示前 200）
Numerical Fuzz：一种面向舍入误差分析的类型系统
提出带线性灵敏度与分级单子的类型系统 Λ_num，静态推导浮点舍入误差的定量界并证明其语义可靠性。
合成后向误差界：后向稳定性
提出可组合的后向稳定性定义与范畴 Shel，并实现工具 eggshel 自动合成数值程序的后向误差界。
带循环的离散概率程序后验分布的保证界
提出残差质量语义与几何界语义，为带循环离散概率程序的后验分布自动计算保证上下界。
Bean：一种用于后向误差分析的语言
提出 Bean 语言及带分级 coeffect 与严格线性的类型系统，静态推导浮点程序后向误差界，并用范畴语义证明可靠性。
ExAIS：神经网络框架的正确性规约与可执行语义
用 Prolog 为 TensorFlow 几乎所有层建立可执行语义，并据此实现 fuzzing 与模型验证。
概率编程中的条件化
在 pGCL 上研究 conditioning 的 wp 与操作语义，证明其对应条件期望奖励，并给出消除 conditioning 的程序变换。
高阶概率程序的形式验证：关于近似、收敛、贝叶斯推断与优化的推理
提出 PPV 逻辑族，用于验证带连续分布和高阶函数概率程序的近似、收敛、贝叶斯推断与优化性质。
对“关于推理的推理”的推理：带嵌套查询与递归的概率程序的语义与上下文等价
首次为含嵌套查询与一般递归的概率程序给出互递归语义，并建立上下文等价的关系推理原则。
多种基测度下的符号化分解
提出首个支持可变基测度的符号化测度分解变换，可检查或推断基测度，并在语义上证明其可靠性。
基于生成函数的循环概率程序精确贝叶斯推断
提出基于生成函数的精确贝叶斯推断，可处理带无界循环的概率程序。
通过资源分解集成资源分析
提出资源分解，将多种资源分析技术组合，并证明组合得到的成本界可靠。
面向高阶概率论的一个方便范畴
提出准博雷尔空间，为高阶概率程序提供兼具连续分布与高阶函数的范畴语义。
Outcome Logic：正确性与不正确性推理的统一基础
提出 Outcome Logic，统一正确性与不正确性推理，并证明错误规约可在其自身中证伪。
带条件化的高阶概率程序语义
用有序 Banach 空间上的线性算子为带条件的高阶概率程序建立指称语义，并验证 Gibbs 采样。
带连续随机变量与递归的概率语言的上下文等价
为含连续随机变量、scoring 与递归的无类型概率语言给出上下文等价的完整推理原则。
骨架语义及其解释
提出骨架语义，用统一解释从语言构造的语义骨架系统导出具体/抽象语义及一致性结果。
基于偏马尔可夫范畴的证据决策论
提出偏马尔可夫范畴，统一刻画带约束、观测与更新的随机过程，并形式化证据决策论。
一种面向条件独立性的束逻辑
扩展 BI 逻辑以非交换合取刻画条件独立，并基于 Markov 核与幂集单子给出模型和概率程序验证逻辑。
工程化一个经过形式验证的自动缺陷查找器
提出用操作语义与符号语义关联来工程化可证明可靠且完备的符号执行缺陷查找器，并在 Coq 中验证 WiSE。
贝叶斯编程的交互几何
为带连续采样与软条件的高阶贝叶斯 λ-演算建立交互几何模型，并证明其对两类操作语义充分。
随机 λ-演算的通用语义
为随机 λ-演算建立可靠且充分的指称语义与操作语义，统一高阶概率程序的语义框架。
概率编程的确定性流采样：语义与验证
提出以采样器为中心的高阶概率语言，给出操作/指称语义，并建立验证采样器正确性的演算。
形式化 Linux eBPF 核心 ISA：机器化操作语义及其真实世界应用
在 Rocq 中形式化 eBPF 核心 ISA 的全部 153 条指令，并据此验证 eBPF 验证器抽象域的可靠性、发现内核缺陷。
一个简单的可微分编程语言
为带反向模式微分的可微分编程语言建立操作语义与指称语义，并证明二者一致。
PCF 中的自动微分
证明 PCF（含实数的高阶图灵完备语言）中前向与反向自动微分在温和假设下几乎处处正确。
混合符号期望的最弱前置期望语义
提出可处理混合符号无界随机变量期望的概率程序最弱前置期望演算，保证语义总良定义且可靠。
概率语言中可靠可编程推断的迹类型与指称语义
提出迹类型系统与指称语义，使可编程推断程序在构造上保证可靠性，覆盖变分、SMC、MCMC 等。
基于度量的概率关系推理
扩展 Fuzz 以支持概率程序的一般关系性质，并用范畴语义刻画概率散度组合，覆盖近似差分隐私。
可证明正确、渐近高效的高阶反向模式自动微分
提出高阶反向模式自动微分的简单高效实现，并证明其正确性与渐近复杂度。
抽象外延性：论不完全抽象解释的性质
将程序外延等价推广到抽象解释诱导的抽象等价，证明任何非平凡抽象解释都会揭示程序的内涵差异。
高阶分离逻辑中的异步概率耦合
提出支持异步概率耦合的高阶概率关系分离逻辑 Clutch，并用于证明高阶程序的上下文精化与等价。
带精确条件化的概率程序的组合语义
为带一阶精确条件化的高斯概率程序建立操作、指称与等式语义，并用范畴构造 Cond 推广精确条件化。
PerSeVerE：ext4 下用于验证的持久性语义
形式化 ext4 与 C/C++ 弱内存的持久性语义，提出模型检测验证方法并发现编辑器缺陷。
加权编程：一种用于规约数学模型的编程范式
提出加权编程范式及 Dijkstra 风格的 wp/wlp 演算，用以规约并推理超出概率分布的数学模型。
连续格上的不动点博弈
提出连续格上的不动点奇偶博弈，统一刻画最小/最大解并推广 progress measure 至格化 µ 演算验证。
抽象解释器的组合式可靠性证明
提出基于共享解释器与 arrow 接口的框架，使抽象解释器的可靠性证明可组合并复用。
带合并的符号求值的形式化基础
首次为支持状态合并的可复用符号求值器建立形式语义，并在 Lean 中机械化证明其可靠性与完备性。
ωPAP 空间：高阶、递归概率与可微程序的指称式推理
提出 ωPAP 空间范畴，为高阶递归概率与可微程序建立指称语义，并证明自动微分与密度计算等正确性。
索引流：融合收缩程序的形式化中间表示
提出索引流：统一稀疏张量与关系代数融合收缩执行的形式化中间表示，证明正确性且性能可比专用系统。
高阶概率对抗计算：范畴语义与程序逻辑
为高阶概率对抗计算建立一元与关系程序逻辑，并在准 Borel 空间范畴中证明可靠性。
抽象抽象机的再函数化：弥合抽象抽象机与抽象定义解释器之间的鸿沟（函数式珍珠）
通过再函数化等语义变换，将小步抽象抽象机系统转化为大步抽象定义解释器，并揭示控制流分析中精确的调用/返回匹配。
HoCHC：一个反驳完备且语义不变的高阶逻辑模理论系统
为高阶约束 Horn 子句提出简单归结证明系统，并证明其在标准与 Henkin 语义下可靠且反驳完备。
Tree Borrows（树状借用）
用树结构替代栈定义 Rust 别名模型 Tree Borrows，更精确刻画 unsafe 代码行为，大幅减少误报并保留与新增编译器优化。
强化学习的形式化规约与测试
为基于时序差分的强化学习提出形式规约，并以DSL解释器作测试预言机进行基于属性的测试与变异评估。
基于操作博弈语义的组合式关系推理
提出 Kripke 范式双模拟，用操作博弈语义统一四类高阶语言的上下文等价关系推理，并证明其可靠完备。
计算图抽象的几何
用动态交互几何为按值λ演算中的计算图抽象建立类型系统与语义模型，保证垃圾回收和β律安全。
用于组合式微分参数不连续性的分布
提出首个可靠微分参数不连续性的一阶可微语言 Potto，并给出指称语义与支持分离编译的高效实现。
CF-GKAT：控制流变换的高效验证
提出 CF-GKAT，扩展 GKAT 以支持非局部控制流和硬编码值，高效可靠完备地验证控制流变换的迹等价。
为 GPU 计算的中间表示夺回控制权
为 SPIR-V 结构化控制流建立形式模型，据此修正规范、校验工具，并用模型引导的模糊测试发现 20 个编译器缺陷。
高阶贝叶斯网络，精确地
提出高阶 λ-演算，可编译为贝叶斯网络，并给出精确、组合且考虑代价的语义。
Java 与 Lambda：一个 Featherweight 故事
提出核心演算 FJ&λ，形式化 Java 8 的 lambda、交集类型与接口默认方法，并证明类型安全与推断。
兴趣分歧的模拟关系家族
提出 μdiv-模拟关系，统一强、弱、发散敏感等 12 种模拟，并在 Rocq 中形式化验证。
可综合 Verilog 的仿真语义
指出现有 Verilog 标准与可综合子集语义的不一致，修复并给出首个可执行真实硬件设计的仿真语义形式化。
Datalog 程序的交互式调试
提出基于自顶向下小步操作语义的 Datalog 交互式调试器，支持 step-into/step-over，并适配 Soufflé 与 IncA。
从操作语义自动派生控制流图生成器
提出从操作语义自动合成多种控制流图生成器的理论、算法与工具 Mandate。
抽象分配：控制流分析中 polyvariance 的统一方法
提出可调抽象分配函数，统一并泛化高阶控制流分析中的 polyvariance，且保证可靠性。
随机变量、条件独立与抽象样本空间范畴
从合适 Markov 范畴构造满足 Simpson 公理的样本空间范畴，并合成式建立概率层理论。
λ演算与概率计算
为λ演算引入概率选择算子，建立按值/按名语义下的合流与标准化理论。
名字生成的概率编程语义
将准Borel空间语义用于ν演算，证明其可靠且在一阶类型上完全抽象，建立随机采样与新鲜名字生成的类比。
全路径可达性逻辑
提出语言无关的全路径可达性逻辑，以操作语义为公理证明非确定性程序的部分正确性。
P4-SpecTec：将语言机械化框架集成到真实世界 P4 规范中
提出 P4-SpecTec，用可执行算法推理规则机械化 P4 静态/动态语义，生成类型检查器与解释器，发现 24 个 bug。
无元素概率分布与随机划分
用多重集和范畴论建立无元素概率分布理论，并给出交换随机划分与随机分布的表示定理。
下推正规形式互模拟：一种面向程序等价的名义上下文无关方法
提出下推正规形式互模拟，可可靠、完备且对调用栈无界情形可判定地验证高阶函数式程序上下文等价。
WebGPU 着色语言中的 Uniformity 分析
首次形式化研究 WebGPU 着色语言的 uniformity 分析，定义 barrier divergence，修正 WGSL 规范并发现 Chromium 实现缺陷。
最优谓词下推合成
提出有状态 fold 计算的最优谓词下推合成框架，自动生成正确且最优的过滤分解。
面向未来 700 种内存模型的组合符号执行
为可参数化内存模型的组合符号执行平台提供新形式基础，并在 Rocq 中机器化。
一种纯需求操作语义及其在程序分析中的应用
提出仅用调用栈和程序点/词法层作为状态的纯需求操作语义，并将其有限化直接导出高阶程序分析。
等价超图：幺半群 E-Graph 的 DPO 重写
为幺半群 e-graph 建立范畴语义与 e-超图表示，并实现 DPO 重写。
概率符号执行的范畴语义
提出“符号集合”语义域，并给出解释器自动正确性元定理。
带有置信度的抽象解释：用概率量化数据流分析的精度
为抽象解释的数据流分析建立概率化置信度理论框架，量化分析结果的局部完备性精度。
谓词转换器语义的充分性
提出通用框架证明谓词转换器语义相对于操作语义的充分性，覆盖无界递归概率高阶程序。
调用守卫的抽象定义式解释器
CGADI 将抽象推迟到参数化安全性质触发时，使系统化抽象框架能在部分执行中保持完全精确而不失可计算性。
证明作为有状态程序：带抽象 Hoare 三元组的一阶逻辑及其到命令式语言的解释
提出带抽象 Hoare 三元组的一阶逻辑，并用可实现性解释将证明抽取为有状态程序。
不动点方程系统上的操作
研究完备格上不动点方程系统在变量代入、方程重排等操作下解保持不变的条件，并提供机器检查证明。
ARMv8-A、RISC-V 和 CHERI-MIPS 的 ISA 语义
使用 Sail 语言为 ARMv8-A、RISC-V、MIPS 和 CHERI-MIPS 架构建立严谨的可执行语义模型，支持模拟器与证明助手代码生成。
交互树：在 Coq 中表示递归与不纯程序
提出交互树，在 Coq 中表示递归、有副作用且可能非终止的程序，支持组合解释与弱互模拟等式推理。
Stacked Borrows：一种面向 Rust 的别名模型
提出 Stacked Borrows 操作语义，为 Rust 定义别名纪律，并用 Coq 证明其足以支撑内存访问重排优化。
抽象定义解释器（函数式珍珠）
提出以定义解释器作为高阶语言抽象解释的基础，并发现抽象定义解释器能自然继承下推控制流精度。
ReLoC：一种用于高阶状态、细粒度并发、多态与递归类型程序精化的逻辑
提出 ReLoC，一种用类型与结构导向规则证明高阶状态、细粒度并发、多态和递归类型程序精化的逻辑。
Aeneas：通过函数式翻译验证 Rust 程序
提出 Aeneas，将 Rust 程序轻量翻译到纯 lambda 演算，免去内存推理并用定理证明器验证函数正确性。
LLVM IR 的模块化、组合式且可执行的形式语义
用 Coq 中 interaction trees 的单子解释为 LLVM IR 大型顺序子集建立模块化、可组合且可执行的形式语义。
状态-效应三角（state-and-effect triangles）的构造配方
利用 Beck 单子性定理，从伴随系统化构造状态-效应三角，统一多种程序语义单子。
面向统计概率编程的域理论
提出 quasi-Borel predomains，为含递归高阶类型与连续概率的统计概率编程语言建立充分指称语义，并证明交换性等价。
下一个 700 种关系程序逻辑
提出首个可为任意单子效应定义关系程序逻辑的通用框架，并给出语义基础与可靠逻辑核心。
可监控性探究：从分支时间到线性时间再返回
建立了带递归 Hennessy-Milner 逻辑的运行时可监控性理论，给出线性时间下可监控片段的表达力层级与监控保证。
在类型论中实现类型论的正规化求值
在类型论内部用商归纳类型构造依赖类型的正规化求值，并证明定义相等可判定。
基于概率进程演算的组合性双模拟度量推理
提出用一致连续性刻画概率进程演算中双模拟度量语义的组合推理，并支持递归过程与度量式假设保证性能验证。
POPLMark 重装上阵：通过逻辑关系机械化证明
提出用Kripke式逻辑关系证明强规范化的基准，比较Beluga、Coq、Agda等证明助手对机械化元理论的支持。
语义引导的程序合成
提出 SemGuS 框架，允许以递归大步步语义定义合成问题，并用 CHC 证明搜索同时合成程序与证明不可实现性。
量子程序的定量鲁棒性分析
为含噪量子 while 程序建立语义与逻辑，定义并证明 ε-鲁棒性，支持纠错方案分析。
通过弱分配律组合概率选择与非确定性选择
证明幂集单子到有限分布单子存在弱分配律，导出凸幂集单子，并应用于概率-非确定系统的迹语义与行为等价。
匹配 μ-逻辑
为匹配逻辑给出可靠完备证明系统，并扩展出匹配 μ-逻辑，统一刻画多种不动点、模态与时序逻辑。
用于成本分析的量子期望变换器
提出混合经典-量子语言的期望变换器语义，可对量子程序做期望成本与期望值分析。
用 SpecTec 为 WebAssembly 标准提速
提出 SpecTec DSL 与工具链，将 Wasm 形式规范作为单一事实来源，自动生成规范文档与元级解释器并发现规范错误。
Choice Trees：在 Coq 中表示非确定性、递归与不纯程序
提出 ctrees，一个在 Coq 中统一建模非确定性、递归与不纯程序并支持双模拟/精化推理的余归纳树单子。
基于导数的、具有回溯语义的真实世界非回溯正则匹配
提出基于导数的非回溯正则匹配算法，支持锚点与计数并保持回溯语义，已在 .NET 7 实现并形式验证。
使用匹配逻辑定义绑定器的一种通用方法
提出用匹配逻辑统一公理化定义对象语言中的绑定器，并给出保守扩展与模型完备性结果。
POSIX shell 的可执行形式语义
为 POSIX shell 定义可执行、机器化的小步操作语义 Smoosh，并通过测试验证其最符合 POSIX 标准。
JISET
针对现代 JavaScript 形式语义人工编写、易错且滞后的问题，论文提出 JISET；所给摘要未展开具体方法。
用效应处理器延续 WebAssembly
提出 WasmFX，用效应处理器为 WebAssembly 增加类型安全的续延与非局部控制流支持。
高效且模块化的余代数划分细化
提出通用余代数划分细化算法，按行为等价商化系统，复杂度 O(m log n)，并统一多种系统类型。
面向摊还分析的指称式递推提取
将递推提取扩展到摊还分析，引入带信用标注的仿射中间语言，并证明其到递推语言的指称正确性。
通过 Call-by-Push-Value 为函数式程序提取递推式
以 Call-by-Push-Value 为中间语言，从高阶递归函数式程序自动提取运行时间递推式，并给出指称代价语义。
双模拟与抽象的博弈
用 Spoiler-Duplicator 博弈统一刻画分支、延迟、η 与弱双模拟，并辅助诊断实现与规约的不一致。
高阶概率程序的近似关系推理
提出 Approxis：面向高阶概率程序近似等价的关系分离逻辑，支持误差信用与逻辑关系，并在 Coq/Iris 中机器化验证多个案例。
面向概率编程语言的可交换单子
在 DCPO 范畴上构造三种概率可交换单子，并为概率不动点演算给出可靠且充分的指称语义。
DimSum：多语言语义与验证的去中心化方法
提出去中心化的多语言语义与验证框架，各语言可独立定义、通过事件与组合子组合，并在 Coq 中验证跨语言编译器。
效应的谓词转换器语义（函数式珍珠）
为异常、状态、非确定性与一般递归等效应提出统一的谓词转换器语义，并导出精化关系。
软件系统的一种行为鲁棒性概念
提出将系统鲁棒性定义为仍能保证目标性质的最大环境偏差行为集合，并给出自动计算方法。
关系验证的对齐代数
提出 BiKAT 代数统一关系验证中的对齐表示，支持等式推理并导出 forall-exists 性质的 RHL 规则。
通过延迟迹的可微因果计算
用范畴论中的延迟迹统一建模因果计算，并给出无需展开的状态网络反向传播微分算子。
弥合分布式系统定性与定量模型之间的语义鸿沟
提出从非时间非概率分布式系统模型到概率时间模型的自动变换，并证明语义一致性，使定性与定量分析共享同一模型。
概率分离逻辑的 nominal 方法
证明概率论中的概率空间乘积分解与概率分离逻辑中的测度论分解在范畴等价意义下等价。
基于 Riesz 空间的概率逻辑
提出 Riesz 模态逻辑，用 Riesz 空间建立概率转移系统性质的对偶理论，并给出可靠完备公理化与概率互模拟刻画。
函数式科学工作流语言 Cuneiform 的计算语义
给出 Cuneiform 的抽象语法、简单类型系统与求值语义，并提供 Erlang 参考实现。
基于符号语义的 Rust 健全借用检查
证明 LLBC 及其符号语义是底层指针语言的正确抽象，可作为健全借用检查器，并使 Aeneas 支持循环。
超越定量代数推理中的非扩张运算
扩展定量等式逻辑以支持广义度量代数与提升意义下的非扩张运算，并公理化概率分布上的Ł–K距离。
酉球中的可实现性
提出基于可实现性的线性代数 λ-演算语义，刻画酉性并导出类型规则，可扩展至经典与量子 λ-演算。
随机 λ-演算的布尔值语义
提出随机 λ-演算的布尔值语义，用测度代数解释高阶概率程序并支持等式推理。
面向可数非确定性与概率选择的步进索引逻辑关系
为含可数非确定性与概率选择的高阶语言构建步进索引逻辑关系，并给出可靠完备的上下文等价理论。
结合非确定性、概率与终止：等式推理与度量推理
给出非确定性、概率与终止组合所得 monad 的呈现，提供程序等价性与距离的等式推理工具。
反向传播作为函子：监督学习的组合视角
将反向传播范畴化：证明梯度下降是从参数化函数到更新规则范畴的 monoidal functor，并引入 request function。
CHERI C 的形式化机器化语义：能力、未定义行为与来源
首次严格全面地定义 CHERI C 语义，涵盖能力、来源与未定义行为，并给出可执行及 Coq 机器化形式。
原子层逻辑（Atomic Sheaf Logic）中的等价与条件独立
提出原子层拓扑语义框架，统一解释变量等价与条件独立，并在经典逻辑中验证基本推理原则。
基于余递归代数的范畴活性检查
用余递归代数与余代数模拟，统一范畴化活性验证中的 ranking function 与 ranking supermartingale。
Decalf：一个有向、带效应且成本感知的逻辑框架
提出 Decalf，用内在前序刻画带效应函数式程序成本界的有向成本感知逻辑框架，并给出单纯集模型。
两阶段无限/有限低级内存模型：在 LLVM IR 抽象层级上协调整数–指针转换、有限空间与 undef
提出两阶段无限/有限内存模型，统一 LLVM IR 的整数指针转换、有限空间与 undef，并证明精化以支持优化。
异步多方会话类型中的崩溃停止故障
提出带崩溃停止故障的异步多方会话类型理论，借助崩溃处理分支与全局语义，证明良类型进程在崩溃下仍保证无死锁与活性。
互模拟距离的即时计算
提出连续时间马尔可夫链互模拟距离的多项式线性规划刻画与高效即时算法，避免穷举状态空间。
马尔可夫决策过程中基于分布的目标
研究 MDP 中基于分布的目标如何在完全信息与部分信息之间取得策略层面的权衡。
在 Coq 中形式化 Core Why3
在 Coq 中为 Why3 逻辑片段建立形式语义，并机器化验证其证明系统与变换的可靠性。
修复用于提取的正则表达式
提出首个基于编程示例的提取型正则合成与修复方法，支持反向引用与环视等扩展。
高阶函数的高阶自动微分
为高阶语言中的前向模式自动微分建立基于 diffeological spaces 的语义正确性证明，并扩展到高阶导数。
论不正确性逻辑与带顶元素和测试的 Kleene 代数
证明 KAT 无法直接表达不正确性逻辑，并提出 TopKAT 通过顶元素刻画陪域，表达不正确性三元组并证明其规则可靠。
状态之间与谓词之间的距离
借助有效关系统一刻画概率状态与谓词上的度量，并应用于经典和量子概率的 state-and-effect 三角。
如何用二阶计算分析器 SOL 证明等式理论的可判定性
提出二阶代数理论下证明等式理论可判定性的通用方法，并实现 Haskell 分析器 SOL。
公平枚举组合子
提出枚举组合子的公平性理论，设计公平组合子并证明其性质，用于属性测试更高效地发现程序语言模型缺陷。
具体范畴与高阶递归
提出一类具体层模型，统一概率与可微编程等语义，并证明通用计算充分性定理。
JavaScript 正则表达式语义的 Coq 机器化
首次在 Coq 中忠实机器化 ECMA-262 的 JavaScript 正则语义，证明匹配必然终止且安全，并可提取为通过 Test262 的引擎。
定量最弱超前置（Weakest Hyper Pre）：通过谓词变换器统一正确性与不正确性超属性
提出定量最弱超前置演算，用谓词变换器统一正确性与不正确性超属性的推理。
基于随机概率的概率编程
提出以随机估计密度比为核心的 PPL，首次同时支持边缘化、嵌套推断、随机控制流与可编程推断。
Verilog 的本质：一种可处理且经测试的 Verilog 操作语义
提出核心语言 λV，为 Verilog 给出覆盖完整特性、可执行且经测试的操作语义，并解决语义陷阱。
计算概率自动机的概率互模拟距离
将概率互模拟距离刻画为随机博弈解，并给出首个实用的策略迭代计算算法。
λS：具有高阶函数与数据类型的可微编程的可计算语义
提出可微编程语言 λS，首次为高阶函数、高阶导数与 Lipschitz 不可微函数提供可计算语义。
概率重写与渐近行为：终止性与唯一范式
为概率重写系统建立分析终止性、唯一极限分布与唯一范式的证明技术，并用于比较归约策略。
在 Event-B 的 institution 中构建规约
为 Event-B 规约语言建立基于 institution 的形式语义，证明其满足性保持与模型合并条件，并统一参数化与精化等模块化构造。
共归纳谓词的可表达逻辑
在共代数上为共归纳谓词建立逻辑完全刻画的一般框架，给出充分条件并实例化相似、发散与行为度量。
论单子式逆向归纳的正确性
定义单子式 SDP 的正确性，给出三个条件证明单子逆向归纳正确，并在 Idris 中形式化。
论并发分离逻辑的代数抽象
论文用PCM间保持结构的部分函数与分离关系，对并发分离逻辑中的所有权转移进行了代数形式化。
概率编程的悖论：以及如何用无穷小概率对零测度事件进行条件化
指出朴素似然累积在条件化零测度事件时导致悖论，并提出用无穷小概率累积执行概率程序来消除悖论。
稳定关系与高阶程序的抽象解释
提出未类型化传值 λ 演算的稳定关系指称语义，并据此导出高阶程序模块化关系分析。
含纯方法调用规约的框架推理逻辑分析
将纯方法与读效应引入区域逻辑，为模块化框架推理建立可靠证明规则并机器检验示例。
实数及其他空间上的可计算决策
提出基于构造拓扑的程序语义，利用非确定性/部分性及空间模式匹配，在精确实数计算中实现可计算的离散决策。
有类型–无类型交互：比较分析
提出统一评估框架，对比若干主流有类型–无类型交互语义，帮助设计者分析自身动态语义的保证。
高阶解释理论及其在 Basic Feasible Functions 中的应用
将解释方法扩展到纯高阶函数式语言，并用高阶多项式刻画任意阶 Basic Feasible Functions。
纯同构类型系统（Pure Iso-Type Systems）
提出 PITS 演算族：以统一语法兼顾项与类型、支持无限制一般递归，并通过 iso-types 与显式 cast 保持类型检查可判定。
分布凸集中的终止性
刻画凸代数单点扩张，为概率系统终止建模提供完整分类，并给出唯一函子性黑洞扩张。
智能选择与选择单子
用选择单子为含选择、奖励与概率的语言建立操作/指称语义，并证明二者一致与完全抽象。
带经典见证的构造性Domain
提出从程序抽取视角出发、以经典正确性断言实现的构造性连续Domain理论，并给出函数空间与实数表示定理。
概率 call-by-name FPC 中的凸性与序
证明 Kegelspitzen 构成概率 call-by-name FPC/pPCF 的指称模型，并讨论概率递归类型解释。
过程间、可能非终止程序中基于依赖切片的语义正确性
为过程间且可能非终止程序上的一类基于依赖的切片方法给出通用语义正确性证明。
高阶需求驱动符号求值
提出 DDSE，一种面向函数式语言的高阶需求驱动符号反向执行，证明其可靠性并用于测试生成。
余代数式无穷轨迹与 Kleisli 模拟
为 Kleisli 模拟建立余代数理论，证明其对无穷轨迹包含的可靠性，并扩展前向部分执行。
验证软件飞地 Hypervisor 中页表的 Rust 实现
为 Rust MIR 提出轻量形式语义与分层证明框架，验证 HyperEnclave 页表配置并证明安全飞地的空间隔离。
随机变量的笛卡尔闭范畴
在 Scott 域框架下构造随机变量域，建立概率编程语义的笛卡尔闭范畴与四个强交换单子。
有限可生成子集的凸包及其谓词变换器
用域论构造有限可生成子集的可计算凸包映射，并导出其谓词变换器。
ArchSem：可复用的宽松架构严格语义
提出架构通用框架 ArchSem，模块化组合 ISA 与并发模型，并在 Rocq/Isabelle 中实例化 Arm/RISC-V 以支持严格验证。
锥上的积分
为可测锥建立积分理论，使概率编程语言的抽样原语可在锥语义模型中获得解释，并构造线性逻辑的两个指数余单子。
OCaml 一个片段的 формальная 语义与程序逻辑
为 OCaml 的一个含效应处理器的顺序片段建立形式语义与两种程序逻辑。
精确实数计算的语义、规约逻辑与霍尔逻辑
提出精确实数计算语言 ERC，给出可计算完备的指称语义、可判定规约逻辑及可靠且表达力强的霍尔逻辑。
无需区间的内部参数性
提出一种无需显式区间或高维立方语法的内部参数性类型论，并以预层与胶合模型证明外部参数性与 canonicity。
libLISA：x86-64 上的指令发现与分析
libLISA 无需人工编写反汇编器，即可自动发现并分析 x86-64 指令，生成 CPU 特定的形式化模型。
无界分离逻辑中的分数资源
提出允许断言求值期间持有超过完整权限的无界分离逻辑语义，统一语义与语法乘法并恢复分配、提取与合并性质。
时序数字电路的完备理论：指称、操作与代数语义
为时序数字电路建立指称、操作与代数三种可靠且完备的语义，并给出观察等价与范式代数理论。
用三维精化代数统一组合式验证与认证编译
提出三维精化代数及其组合语义框架，并在 Coq 中统一组合式验证与认证编译。
组合式不精确概率：分级单子与 Markov 范畴的解决方案
用命名不确定选择与分级单子，在 Markov 范畴中为不精确概率给出全组合语义，并获得更紧界。
用于高效 WebAssembly 机器化的 Progressful 解释器
提出 progressful 解释器，用 Coq 依赖类型认证健全性与 progress，高效扩展 Wasm 2.0 机器化。
通过后向分析揭示（内存）错误来源
提出后向欠近似的 SIL 与 Separation SIL 证明系统，定位错误来源并处理指针与动态内存错误。
随机图的概率编程接口：马尔可夫范畴、graphon 与名义集合
建立图上概率编程语义与 graphon 的对应，并给出三种构造证明每个 graphon 均可由等式理论产生。
基于划分精化的双模拟判定算法下界
证明了使用划分精化的顺序与并行双模拟判定算法的时间下界，分别为 Ω((m+n) log n) 与 Ω(n)。
向 λμ-演算中添加否定
在 Parigot 的 λμ-演算中引入否定类型构造及语法构造，并证明其归约合流、强规范化与主类型性质。
通过抽象单子实现灵活的指令集语义（经验报告）
提出用 Haskell 子集和抽象单子编写可复用的指令集语义，以同一核心语义支持测试、交互证明与软硬件模型检测。
指称语义作为函数式语言代价递推提取的基础
以指称语义形式化函数式程序的代价递推提取：先用单子翻译提取代价，再借不同模型刻画不同的规模概念。
通过范畴论逻辑关系构造有效应 λ-演算的完全抽象模型
提出范畴论逻辑关系构造，为带和类型、效应操作与基元的计算 λ-演算生成可靠且完全抽象的模型。
面向并行 Unix 管道的有序感知数据流模型
提出顺序感知的数据流模型以精确刻画并行 Unix 管道语义，并证明其并行化变换的正确性。
参数多态与操作式改进
提出对时间开销敏感的操作式参数性理论，用于证明程序融合是时间改进。
非确定性与概率 Büchi 自动机的公平模拟：一个余代数视角
从余代数视角统一推广 Büchi 自动机的公平模拟至非确定树自动机与概率字自动机，并证明其可靠性。
Hoare 式逻辑的分类学：基于谓词变换器与带顶和测试的 Kleene 代数走向整体视角
通过谓词变换器和 TopKAT 建立类 Hoare 逻辑的分类学，并给出 Lisbon 逻辑的新 TopKAT 刻画。
通过 Filtered-Simulation 弥合真实世界与形式化二进制提升之间的差距
提出 filtered-simulation 刻画真实二进制提升中启发式假设的正确性，并形式化三种核心变换。
带测试与顶元素的 Kleene 代数的完备性定理
证明了带测试与顶元素的 Kleene 代数的两个完备性定理，并给出二元关系等式理论的 PSpace 算法。
形式化图变换的双推出（DPO）方法
在 Isabelle/HOL 中形式化双推出图变换基础理论，并机器验证推导唯一性与 Church-Rosser 定理。
Shoggoth：策略重写的形式化基础
提出 Shoggoth，为策略重写建立指称语义与基于位置的弱前置条件演算，并在 Isabelle/HOL 中机化验证。
崩溃下线性一致性的组合性与观测精化
提出带崩溃的并发计算组合模型和 crash-aware linearizability，并给出首个验证崩溃下线性一致性的程序逻辑。
不动点理论——颠倒视角
提出证明元素高于最大不动点或低于最小不动点的证明规则，并用有限逼近与 MV-代数格统一处理概率/度量语义及随机博弈。
带 Frame 的一阶逻辑
提出 Frame Logic，扩展一阶逻辑与递归定义，用支持集实现 frame reasoning，并用于堆程序局部规范。
强分离逻辑
提出强分离逻辑，通过限制分离合取的语义，在保留魔法棒和归纳谓词的同时恢复可判定性。
面向 Eilenberg--Moore 代数的代数语言理论
提出基于 Eilenberg--Moore 代数的代数语言理论，支持无限多 sort 的代数并借助可定义代数连接逻辑。
一种建立服务级别协议的对称协议
提出一种双方动态协商服务等级的对称协议，并用模态公式与行为归约验证其正确性。
概率高阶语言的环境互模拟
为概率高阶语言定义环境互模拟，并证明其相对于上下文前序与上下文等价的全抽象性。
结合不动点理论与微分理论
提出带不动点算子的笛卡尔微分范畴，并用新公理刻画微分与不动点的交互，应用于 Newton-Raphson 优化。