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
标签：量子与概率编程（共 392 篇，按优先级展示前 200）
迈向概率程序的已验证随机变分推断
形式化随机变分推断中 REINFORCE 的隐含假设，并实现 Pyro 静态分析验证 model-guide 支撑匹配。
通过多项式求解的贝叶斯概率程序静态后验推断
提出用多项式求解静态推断贝叶斯概率程序的归一化后验分布边界，并支持 score 递归程序。
带循环的离散概率程序后验分布的保证界
提出残差质量语义与几何界语义，为带循环离散概率程序的后验分布自动计算保证上下界。
概率程序的平滑性分析及其在优化变分推断中的应用
提出概率程序平滑性静态分析，自动识别可微部分，改进路径梯度估计器且无需人工干预。
贝叶斯分离逻辑：概率编程的逻辑基础与公理语义
提出贝叶斯分离逻辑 BaSL，为贝叶斯概率编程提供逻辑基础与公理语义，并支持贝叶斯更新等模块化推理。
带用户标注采样语句与 while 循环的概率程序的静态因子分解
为含用户标注采样语句与 while 循环的概率程序给出静态因子分解与程序切片，并据此加速概率推断优化。
通过类型系统刻画条件独立性
提出信息流类型系统捕获概率模型的条件独立性，并用类型推断与程序变换自动消除离散参数。
基于矩匹配高斯混合的概率程序推断
提出高斯语义，用矩匹配高斯混合逼近概率程序语义，并证明通用逼近定理与二阶矩算法 SOGA。
可编程 MCMC 与可靠组合的引导程序
提出基于协程和类型系统的框架，验证可编程 MCMC 中用户引导程序的正确性与可组合性。
概率编程中的条件化
在 pGCL 上研究 conditioning 的 wp 与操作语义，证明其对应条件期望奖励，并给出消除 conditioning 的程序变换。
从概率函数式程序推导概率密度函数
提出一种概率函数式语言的密度编译器，并为含失败及离散/连续分布的程序证明其可靠性。
定量分离逻辑：一种推理概率指针程序的逻辑
提出定量分离逻辑 QSL，为概率指针程序提供带局部推理的定量最弱前置条件演算。
高阶概率程序的形式验证：关于近似、收敛、贝叶斯推断与优化的推理
提出 PPV 逻辑族，用于验证带连续分布和高阶函数概率程序的近似、收敛、贝叶斯推断与优化性质。
面向自动数据建模的概率程序的贝叶斯合成
提出概率程序的贝叶斯合成框架，从观测数据自动构造数据建模 DSL 程序并保证其可靠性。
对“关于推理的推理”的推理：带嵌套查询与递归的概率程序的语义与上下文等价
首次为含嵌套查询与一般递归的概率程序给出互递归语义，并建立上下文等价的关系推理原则。
多种基测度下的符号化分解
提出首个支持可变基测度的符号化测度分解变换，可检查或推断基测度，并在语义上证明其可靠性。
Bit Blasting 概率程序
提出 bit blasting 离散化，将混合概率程序转为布尔随机变量上的离散推断，并实现 HyBit。
基于生成函数的循环概率程序精确贝叶斯推断
提出基于生成函数的精确贝叶斯推断，可处理带无界循环的概率程序。
基于信息流的概率程序编译与变量消除
提出一种编译方法，利用信息流类型系统分解概率计算，将递归概率程序的全局边缘推断化为可处理子问题。
命令式概率程序的切片理论
提出命令式概率程序的切片理论，给出语法条件、语义正确性证明与最小切片算法。
混合粒子滤波的推断计划
提出推断计划接口与 Siren 语言，让开发者控制混合粒子滤波的变量划分，并用抽象解释静态分析判定其可满足性。
概率程序的语言无关静态分析
提出语言无关的概率程序静态分析框架 LASAPP，支持五种概率语言并实现四类可证正确的分析。
概率程序中高效可编程推断的增量计算
将概率程序编译为密度函数并增量计算，加速多种蒙特卡洛推断且分离式证明保证正确性。
面向高阶概率论的一个方便范畴
提出准博雷尔空间，为高阶概率程序提供兼具连续分布与高阶函数的范畴语义。
低目标更难：概率程序验证中用于下界的归纳法
提出无需序列极限、仅需有限次应用循环体语义的概率程序期望值与运行时间下界归纳验证规则。
带条件化的高阶概率程序语义
用有序 Banach 空间上的线性算子为带条件的高阶概率程序建立指称语义，并验证 Gibbs 采样。
概率循环的时刻已经到来
提出全自动静态分析，为一大类概率循环精确推导程序变量高阶矩，无需外部不变式或模板。
带连续随机变量与递归的概率语言的上下文等价
为含连续随机变量、scoring 与递归的无类型概率语言给出上下文等价的完整推理原则。
Storm：面向概率编程系统测试与调试的程序归约
提出 Storm，通过程序归约帮助定位概率程序在概率编程系统中引发失败的代码片段。
Lilac：一种面向条件概率的模态分离逻辑
提出 Lilac 分离逻辑，以分离合取刻画概率独立性，并基于 disintegration theory 引入条件概率模态。
基于偏马尔可夫范畴的证据决策论
提出偏马尔可夫范畴，统一刻画带约束、观测与更新的随机过程，并形式化证据决策论。
BlueBell：关系提升与独立性的联盟及其在概率推理中的应用
提出概率程序逻辑 BlueBell，以“联合条件化”模态统一一元式与关系式概率推理。
一种面向条件独立性的束逻辑
扩展 BI 逻辑以非交换合取刻画条件独立，并基于 Markov 核与幂集单子给出模型和概率程序验证逻辑。
支持可编程变分推断的概率编程
提出以组合式程序变换支持可编程变分推断，将变分目标写成程序并自动变换为无偏梯度估计器。
证明具有随机化、依赖于变量的终止时间的概率程序的期望敏感性
提出基于鞅的可靠方法，证明迭代次数随机依赖输入的概率 while 循环的期望敏感性，并可自动化与组合。
在 SlicStan 中基于密度的概率编程：高效、灵活且确定性
为 Stan 给出基于密度的操作语义，并设计可组合、自优化的 SlicStan，再保义翻译回 Stan。
正几乎必然终止：复杂度与证明规则
证明概率程序的PAST复杂度为Π^1_1完全，并给出基于超限序数的可靠完备证明规则。
用于贝叶斯编程的仿射单子与惰性结构
提出用于贝叶斯编程的仿射概率单子与惰性结构语义，给出适配惰性的推断方法及 Haskell 库 LazyPPL。
概率程序中数组的符号化条件化
将符号化分解算法扩展到概率程序中的数组，实现无需展开循环的提升式条件化。
贝叶斯编程的交互几何
为带连续采样与软条件的高阶贝叶斯 λ-演算建立交互几何模型，并证明其对两类操作语义充分。
强不变式很难：论（概率）程序最强多项式不变式的困难性
证明单路径多项式循环的最强多项式不变式计算至少与 Skolem 问题同难，并推广到概率程序的矩不变式。
类型保持、依赖感知的 guide 生成：面向可靠且有效的摊销概率推断
用行为类型系统驱动类型导向翻译，自动生成概率程序的 guide，保证可靠性并提升摊销推断效果。
随机 λ-演算的通用语义
为随机 λ-演算建立可靠且充分的指称语义与操作语义，统一高阶概率程序的语义框架。
递归程序的自动化期望值分析
提出将前期望语义翻译为一阶约束的项表示，实现递归概率程序期望值的全自动推断。
概率编程语言的验证密度编译
提出 ProbCompCert：用 Coq 验证 Stan 子集概率编程语言编译器的关键遍，并发现 Stan 手册错误。
安全耦合：耦合式精化类型
受概率耦合启发扩展精化类型，在 Liquid Haskell 中验证概率计算的关系性质与机器学习实现。
概率编程的确定性流采样：语义与验证
提出以采样器为中心的高阶概率语言，给出操作/指称语义，并建立验证采样器正确性的演算。
从带循环与条件化的概率程序到形式验证的采样器
提出经 Coq 形式验证的 Zar 编译器，将带循环与条件化的离散概率程序编译为正确采样器。
通过自动循环向量化优化概率程序中的密度计算
提出可靠的自动循环向量化方法，用推测并行与不动点检查加速概率程序推断。
Roulette：一种表达力强、精确且高效的离散概率编程语言
提出 Roulette，首个兼具高性能精确推断与通用语言特性的离散概率编程语言。
用生成函数编译
提出以生成函数为编译目标的概率程序精确推断方法，形式化编译并证明其正确性，实现系统 Geni。
概率程序的牛顿式程序分析
提出 NPA-PMA 框架，将牛顿法程序分析推广到含非确定性、非结构化控制流和递归的概率程序数据流分析。
连续概率程序演绎验证的基础：从勒贝格到黎曼再返回
提出用黎曼和近似积分，将连续概率程序的期望界验证归约为 SMT 不变量验证，并证明收敛与 coRE 完全性。
在线与交互式贝叶斯推断调试
提出在开发环境中在线交互式调试贝叶斯推断的方法与工具，显著降低调试时间与难度。
热带数学与λ演算 II：概率编程语言的热带几何
将热带几何用于高阶概率程序的统计推断，并设计交集类型系统组合式估计最可能运行。
具有向量化可编程推断的概率编程
提出 GenJAX 语言与编译器，将 vmap 向量化引入可编程概率推断，并证明其模型与推断操作向量化的正确性。
noDice：面向带非确定性与条件化的离散概率程序的推断
提出 noDice，扩展 Dice 以对含非确定性与条件化的离散概率程序进行推断，并用决策图缩减所构造 MDP 的状态空间。
通过编译扩展不确定性之上的优化
提出带分支定界半环的二元决策图IR，将概率优化编译为可扩展的推断与优化流程。
带相关输入的概率 Datalog 推断
提出 Praline，扩展 Datalog 以在输入事实相关时进行精确概率推断，并用 δ-exact 算法高效求出紧的概率界。
概率程序的类型导向离散化
提出类型导向的全局变换 Slice，将连续概率程序精确离散化，保持语义并赋能离散推断引擎。
具有形式化保证的随机变量生成
提出从有限精度 CDF 数值程序自动合成精确随机变量生成器的方法，兼具形式化保证与熵最优性。
测试概率编程系统
表征概率编程系统缺陷并提出可扩展测试工具 ProbFuzz，发现大量真实 bug。
提升期望：用类型自动进行期望成本分析
提出基于类型的概率程序期望执行成本上界分析，支持高阶函数与归纳数据类型，并将推断归约为线性约束求解。
概率程序的相对完备验证：一种用于基于期望推理的表达性语言
提出一种表达力充分的定量断言语法，使概率程序基于期望的验证系统达到相对完备。
概率终止的可靠且完备证明规则
为带离散概率选择与有界恶魔非确定性的命令式程序，给出算术断言语言中可靠且相对完备的定性/定量概率终止证明规则。
概率语言中可靠可编程推断的迹类型与指称语义
提出迹类型系统与指称语义，使可编程推断程序在构造上保证可靠性，覆盖变分、SMC、MCMC 等。
AcMC²：将概率模型编译为优化的 MCMC 硬件加速器
提出 AcMC² 编译器，将概率模型转换为基于 MCMC 的 FPGA/ASIC 硬件加速器，并通过依赖分析优化并行与数据局部性。
概率敏感性的前期望演算
提出关系前期望演算，用Kantorovich距离上界约束概率程序两次执行输出的分布距离。
错误信用：面向高阶概率程序错误界的有资源推理
提出 Eris 高阶分离逻辑与错误信用，证明高阶概率程序的精确错误概率上界。
面向概率程序的演绎验证基础设施
提出首个面向概率程序的演绎验证基础设施，用实值逻辑、中间验证语言与最弱前置条件支持期望型性质的自动验证。
带精确条件化的概率程序的组合语义
为带一阶精确条件化的高斯概率程序建立操作、指称与等式语义，并用范畴构造 Cond 推广精确条件化。
面向模块化贝叶斯推断的函数式编程
提出用函数式语言特性实现模块化概率编程库，可组合出最先进的贝叶斯推断算法。
概率函数式程序的基于类型的复杂度分析
提出 λRPCF 类型系统，通过动态分布类型与 Lyapunov 秩函数，对概率高阶函数式程序进行组合式平均情形复杂度分析。
一种用于负相关性的分离逻辑
提出概率分离逻辑 LINA，用两种分离合取分别刻画独立性与负相关性，并验证哈希数据结构等随机程序。
CFLOBDDs：上下文无关语言有序二元决策图
提出 CFLOBDD，一种可替代 BDD 的布尔函数压缩表示，最佳情况下比 BDD 指数级更小、比决策树双指数级更小。
概率程序资源使用量的定量界
结合代价鞅与定量安全性分析，为概率程序给出期望和尾部资源界，突破非负代价、有界更新与期望有限等限制。
ADEV：概率程序期望值的健全自动微分
提出 ADEV，将前向自动微分扩展到概率程序，使变换后程序的期望值等于原程序期望的梯度。
一种定量概率关系霍尔逻辑
提出定量概率关系霍尔逻辑 eRHL，克服 pRHL/apRHL 的随机对齐限制，并给出可靠性与完备性结果。
可能发散的概率程序的下界
提出不依赖几乎必然终止的新证明规则，为可能发散的概率程序建立终止概率与期望值的非平凡下界。
面向运行时概率模型检验的区间变化点检测
提出高效区间变点检测并与贝叶斯估计器集成，使运行时概率模型检验能应对参数突变。
精确递归概率编程
提出一种概率编程语言，可自然表达递归数据上的递归，并通过类型保证的程序变换实现精确推断。
ωPAP 空间：高阶、递归概率与可微程序的指称式推理
提出 ωPAP 空间范畴，为高阶递归概率与可微程序建立指称语义，并证明自动微分与密度计算等正确性。
面向高效流式概率编程的半符号推断
提出半符号推断，使运行时自动实现 Rao-Blackwellized 粒子滤波，精确优先、必要时采样。
高阶概率对抗计算：范畴语义与程序逻辑
为高阶概率对抗计算建立一元与关系程序逻辑，并在准 Borel 空间范畴中证明可靠性。
上鞅、秩函数与概率 λ 演算
提出基于秩上鞅的概率λ演算几乎必然终止证明方法，并给出反单调、稀疏与替代归约策略下的扩展。
基于依赖细化类型系统的高阶概率程序自动验证
提出依赖细化类型系统，将高阶概率程序的多种定量性质验证归约到扩展 CHC 求解，并可复用现有求解器。
高阶概率程序中期望代价的模态类型论
提出 pλ-amor，用分级模态类型论证明高阶概率程序的期望代价界。
通过代数效应实现模块化概率模型
提出基于代数效应的嵌入式 DSL，使概率模型模块化、可复用，并统一支持模拟与推断。
概率程序的等价性与相似性反驳
提出首个全自动、可处理无限状态、带形式保证的概率程序等价性与相似性反驳方法
高阶贝叶斯网络，精确地
提出高阶 λ-演算，可编译为贝叶斯网络，并给出精确、组合且考虑代价的语义。
面向概率程序分析的符号并行自适应重要性采样
提出 SYMPAIS，结合符号执行、重要性采样与约束求解，准确估计高维相关输入下概率程序稀有事件的发生概率。
概率高阶递归程序的终止问题
提出 PHORS 概率高阶程序模型，证明二阶几乎必然终止不可判定，并给出终止概率的不动点刻画与近似算法。
并发概率程序错误概率界的模块化推理
提出首个高阶并发概率程序错误概率界推理的分离逻辑 Coneris，支持随机化逻辑原子性并由 Rocq/Iris 机器化验证。
随机变量、条件独立与抽象样本空间范畴
从合适 Markov 范畴构造满足 Simpson 公理的样本空间范畴，并合成式建立概率层理论。
λ演算与概率计算
为λ演算引入概率选择算子，建立按值/按名语义下的合流与标准化理论。
多语言概率编程
提出 Multi PPL，使精确离散推断与重要性采样两种概率编程语言可靠互操作，并证明推断算法可靠性。
面向离散概率程序推断的随机惰性知识编译
提出随机惰性知识编译，使离散概率程序的精确推断可惰性加速，并用序列蒙特卡洛实现近似推断。
名字生成的概率编程语义
将准Borel空间语义用于ν演算，证明其可靠且在一阶类型上完全抽象，建立随机采样与新鲜名字生成的类比。
量子线路的精确推断：面向量子软件栈的测试预言
提出 QASMInfer，为 OpenQASM 量子线路提供精确概率推断，作为量子软件栈的统一测试预言，发现 31 个缺陷。
无元素概率分布与随机划分
用多重集和范畴论建立无元素概率分布理论，并给出交换随机划分与随机分布的表示定理。
面向 PRISM 的概率编排语言
提出一种概率编排语言，定义概率语义并编码到 PRISM，支持并发概率系统的全局建模与模型检测。
面向现代硬件的可编程分治-合并推断的概率编程
Upix 是首个把分治-合并（DCC）推断实现为框架的概率编程系统，可将通用模型拆分并编译到加速器上高效推断。
PSMT：当可满足性模理论遇到概率分布
提出 PSMT 问题与 Prob-MCSAT 算法，将概率分布引入 SMT 求解，使解呈现合理的分布趋势。
概率符号执行的范畴语义
提出“符号集合”语义域，并给出解释器自动正确性元定理。
LazyHMC：面向惰性、无限维概率程序的 Hamiltonian Monte Carlo 模拟
提出在惰性函数式概率程序中实现无限维参数空间上的梯度型 HMC 与 NUTS，并用 PACAP 分析保证梯度有限支撑。
谓词转换器语义的充分性
提出通用框架证明谓词转换器语义相对于操作语义的充分性，覆盖无界递归概率高阶程序。
量子关系霍尔逻辑（qRHL）
提出量子关系霍尔逻辑 qRHL，用于推理成对交互式量子程序并支持量子密码安全证明。
驾驭可配置软件系统性能估计中的不确定性
提出基于概率编程的 P4，为可配置系统性能影响建模引入不确定性量化与置信区间。
仿射概率程序定性与定量终止问题的算法分析
本文用线性 ranking supermartingale 合成，对仿射概率程序的终止性定性与定量问题给出算法及复杂度界。
面向统计概率编程的域理论
提出 quasi-Borel predomains，为含递归高阶类型与连续概率的统计概率编程语言建立充分指称语义，并证明交换性等价。
基于自动机的量子电路验证与缺陷发现框架
提出基于树自动机的量子电路验证与缺陷发现框架，可验证大型电路并捕获注入缺陷。
随机程序中用于可达性的秩上鞅与排斥上鞅
为随机程序可达概率的上/下近似统一基于鞅的方法，并提出秩上鞅与排斥上鞅两类新技术。
量子程序的定量鲁棒性分析
为含噪量子 while 程序建立语义与逻辑，定义并证明 ε-鲁棒性，支持纠错方案分析。
量子程序的关系证明
提出基于量子耦合的关系程序逻辑，用于验证量子程序的关系性质。
一种摊还期望运行时间演算
提出 aert 演算，以最弱前置条件风格定量推理随机算法在动态内存下的摊还期望运行时间。
基于单子仿射大小类型的概率终止
提出单子仿射大小类型系统，可类型化概率高阶程序并证明其几乎必然终止。
用于成本分析的量子期望变换器
提出混合经典-量子语言的期望变换器语义，可对量子程序做期望成本与期望值分析。
高阶概率程序的近似关系推理
提出 Approxis：面向高阶概率程序近似等价的关系分离逻辑，支持误差信用与逻辑关系，并在 Coq/Iris 中机器化验证多个案例。
面向概率编程语言的可交换单子
在 DCPO 范畴上构造三种概率可交换单子，并为概率不动点演算给出可靠且充分的指称语义。
概率模追踪抽象
提出用失败自动机上近似程序 trace、并将概率推理归约为逻辑推理的概率程序精度验证方法。
面向随机化程序的符号执行
提出可处理随机抽样的符号执行方法，能在未知输入下验证随机化程序的概率性质与期望值。
经验证的量子 oracle 编译
提出 Coq 中实现的高保障框架 VQO，形式验证从 OQIMP 到 OQASM 再到 SQIR 的量子 oracle 编译器，并用 QFT 降低量子比特开销。
论续延传递变换与期望成本分析
为带概率选择、递归与成本计量的λ演算定义CPS变换，使表达式应用于续延λv.0即得期望成本，并给出可靠的高阶逻辑EHOL推导紧界。
Curry 与 Howard 遇上 Borel
建立计数命题逻辑与概率事件 λ 演算的 Curry-Howard 对应，并以交集类型精确刻画概率行为。
面向随机非确定性的 Demonic Outcome Logic
提出 Demonic Outcome Logic，统一推理同时含随机选择与恶魔非确定性的程序，并支持循环终止与结果分布量化。
离散概率分布的 Hyper 正规化与条件化
将概率正规化从偏函数重构为输出分布之分布的全函数，并用于条件化与定量信息流 refinement。
酉球中的可实现性
提出基于可实现性的线性代数 λ-演算语义，刻画酉性并导出类型规则，可扩展至经典与量子 λ-演算。
随机 λ-演算的布尔值语义
提出随机 λ-演算的布尔值语义，用测度代数解释高阶概率程序并支持等式推理。
量子电路描述语言中灵活的基于类型的资源估计
为 Quipper 设计基于效应与细化类型的类型系统，自动推导电路宽度、深度、门数等资源上界。
面向量子程序优化的线性与非线性关系分析
将相位折叠重铸为仿射关系分析，借助经典关系域把优化扩展到含复杂控制流的量子程序。
面向可数非确定性与概率选择的步进索引逻辑关系
为含可数非确定性与概率选择的高阶语言构建步进索引逻辑关系，并给出可靠完备的上下文等价理论。
程序化策略合成：消解概率程序中的非确定性
提出基于最弱前置条件的演绎框架，半自动地为含随机与纯非确定的命令式程序合成无记忆确定性策略，使其满足期望界等定量规约。
加权上下文无关语言有序二叉决策图（WCFLOBDDs）
提出带过程调用机制的层次化加权决策图 WCFLOBDDs，在量子线路模拟中兼顾 WBDD 与 CFLOBDD 的优势。
自动化 Dirac 记号中的等式证明
证明 Dirac 记号的一阶理论可判定，并用项重写高效判定等式，实现等价性检查器。
递归量子酉程序合成的可行性论证
提出首个量子酉程序合成框架 QSynth，借助 SMT 求解自动合成递归定义的量子酉电路。
状态之间与谓词之间的距离
借助有效关系统一刻画概率状态与谓词上的度量，并应用于经典和量子概率的 state-and-effect 三角。
从高层推断算法到高效代码
提出编译方法，将含数组隐变量与共轭似然的高层概率推断程序转换为高效代码。
GenSQL：一个用于查询数据库表生成模型的概率编程系统
在 SQL 上增加少量概率查询原语，构建可查询表格数据生成模型的概率编程系统 GenSQL，并给出类型系统、指称语义与可靠性证明。
定量最弱超前置（Weakest Hyper Pre）：通过谓词变换器统一正确性与不正确性超属性
提出定量最弱超前置演算，用谓词变换器统一正确性与不正确性超属性的推理。
一个在不可预测环境中度量程序鲁棒性的框架
提出基于随机变量序列与概率分布度量的程序鲁棒性框架，并定义适应性与可靠性及统计推断评估算法。
基于随机概率的概率编程
提出以随机估计密度比为核心的 PPL，首次同时支持边缘化、嵌套推断、随机控制流与可编程推断。
通过守卫精化的几乎必然终止证明
提出 Caliper：用保持终止的高阶程序—概率模型精化，经守卫递归与 Löb 归纳证明几乎必然终止。
概率编程的悖论：以及如何用无穷小概率对零测度事件进行条件化
指出朴素似然累积在条件化零测度事件时导致悖论，并提出用无穷小概率累积执行概率程序来消除悖论。
为量子比特映射与路由生成编译器
提出设备状态机抽象与DSL，可自动为任意量子处理器生成量子比特映射与路由编译器。
递归定义量子电路的验证
提出递归定义量子电路正确性的证明系统，并证明其可靠性与相对完备性。
基于效应类型与线性依赖的电路宽度估计
提出 Proto-Quipper-R，用线性依赖类型与效应系统推导电路宽度参数上界，并实现 QuRA 工具验证。
量子比特回收再审视
提出量子比特依赖图，将量子比特回收归约为矩阵三角化，给出 NP 难性、启发式求解器与 Coq 验证实现。
论一阶逻辑二变量片段中的精确采样
证明 FO2 及其带计数约束扩展在采样意义下具有域可提升性，给出多项式时间精确采样算法。
智能选择与选择单子
用选择单子为含选择、奖励与概率的语言建立操作/指称语义，并证明二者一致与完全抽象。
概率 call-by-name FPC 中的凸性与序
证明 Kegelspitzen 构成概率 call-by-name FPC/pPCF 的指称模型，并讨论概率递归类型解释。
随机变量的笛卡尔闭范畴
在 Scott 域框架下构造随机变量域，建立概率编程语义的笛卡尔闭范畴与四个强交换单子。
有限域上概率程序的通用等价与多数性
研究有限域上概率程序等价的可判定性与复杂度，证明通用等价可判定并给出双指数上界。
锥上的积分
为可测锥建立积分理论，使概率编程语言的抽样原语可在锥语义模型中获得解释，并构造线性逻辑的两个指数余单子。
唯一不动点的超鞅：一种下界验证的统一方法
提出以超鞅见证不动点唯一性的统一框架，用于概率程序多种定量性质的下界验证。
组合式不精确概率：分级单子与 Markov 范畴的解决方案
用命名不确定选择与分级单子，在 Markov 范畴中为不精确概率给出全组合语义，并获得更紧界。
随机图的概率编程接口：马尔可夫范畴、graphon 与名义集合
建立图上概率编程语义与 graphon 的对应，并给出三种构造证明每个 graphon 均可由等式理论产生。
渐进概率 lambda 演算
提出并形式化 GPLC，首个渐进类型的概率 lambda 演算，证明其类型安全并满足渐进保证。
离散概率分布的最优近似采样
提出离散分布近似采样的理论框架，并构造在 k 位精度下统计与熵消耗均最优的采样算法。
量子程序中的脏量子比特借用
形式化定义量子程序中脏量子比特借用的语义，提出安全反计算概念，并给出高效验证算法。
SAQR-QC：面向量子电路的可扩展近似定量推理逻辑
提出 SAQR-QC 逻辑，通过可控精度损失和局部推理，实现对大规模量子电路的可扩展近似定量验证。
MarQSim：在量子模拟的编译器优化中协调确定性与随机性
提出 MarQSim 编译框架，用马尔可夫链与最小费用流统一量子哈密顿模拟编译中的确定性与随机性优化。
memo：一个用于推理“推理”的领域特定概率编程语言（或：关于 memo 的备忘录）
提出领域特定概率编程语言 memo，以专用语法语义和数组编程推断，支持心智理论建模。
概率高阶递归程序的终止性问题
提出PHORS模型，证明二阶几乎必然终止不可判定，并给出终止概率的不动点刻画与近似算法。
KQFuzz：面向量子库的基于大语言模型的知识引导模糊测试
提出知识引导的LLM量子库模糊测试方法，结合代码库知识、适应度评估与两级变异，提升覆盖率并发现真实缺陷。
增强量子中间表示（QIR）中的代码安全性
为 QIR 的数据类型与指令集给出形式化定义，以保障量子中间代码操作与转换的正确性与安全性。
从分布上的多重集到多重集上的分布
本文构造并刻画多重集单子到分布单子的分配律，统一非确定性与概率语义并应用于采样语义。
高阶并发概率程序的上下文精化
提出首个用于证明高阶并发概率程序上下文精化的高阶分离逻辑 Foxtrot，并在 Rocq/Iris 中机器化验证。
在守卫类型论中建模递归与概率选择
在守卫类型论中为带概率选择与递归类型的 FPC⊕ 建立操作与指称语义，并支持充分性与上下文等价推理。
一种量化量子网络行为的语言
提出 PBKAT，一种面向量子网络 Bell pair 分发协议的概率/可能性行为规约、验证与定量分析语言及工具。
调优随机生成器：将基于属性的测试视为概率编程
把生成器的随机选择权重视为可学习参数，在离散概率编程系统中自动离线优化测试输入分布，显著提升找 bug 效率。
论 Feller 连续性与完全抽象
引入 Feller 连续性，证明连续采样 λ 演算中多种程序等价与上下文等价一致。
概率逻辑编程的余代数语义
用余代数模型为概率逻辑编程及加权逻辑编程建立语义，给出推导树与可能世界解释并恢复分布语义。
论高阶概率子递归
研究给 Gödel T 加入不同概率选择算子后的表达力，证明它们均几乎必然终止但可生成不同的分布类。
基于概率编程的量子蒙特卡洛估计
提出 QPPL 语言与编译器，将概率程序编译为量子线路，以加速蒙特卡洛估计并保证语义保持。
使用自动机验证 Repeat-until-Success 协议
提出基于层同步树自动机的全自动框架，验证 RUS 量子协议的功能正确性并发现文献中的新 bug。
紧凑且表达力强的量子电路优化的合成
提出 QSymb，自动合成紧凑且具形式保证的量子电路重写规则，显著减少两比特门数量。
QSolver：一种量子约束求解器
提出首个量子约束求解器 QSolver，将量子程序与多时刻约束符号化并用 SMT 求解满足约束的量子态。
当抽象违背物理：重新思考量子软件中的模块化设计
揭示量子软件中经典抽象与量子物理约束的根本冲突，并提出面向量子语义的安全抽象设计原则。
混合量子程序的 Hybrid Path-Sums
提出 Hybrid Path-Sums 符号表示与重写/断言系统，实现混合量子程序的自动形式化验证。
面向量子电路优化的等式饱和
提出 Quasar，用双 e-graph 的等式饱和在限定重写步数内生成量子电路的最低代价优化。
GradInf：梯度估计作为概率推断
提出梯度推断，将概率程序梯度估计归约为概率推断，并实现 GradInf 系统自动构造高效估计器。
浅层量子电路的可扩展等价性检查与验证
提出基于投影的等价性检查 PBEC，可在经典计算机上以对量子比特数线性时间/空间验证浅层量子电路等价性。
Zeta 函数与马尔可夫过程的（线性）逻辑
揭示 Zeta 函数与程序执行的 cocycle 联系，并为 sub-Markov 过程建立二阶线性逻辑模型。
并非所有量子比特生而平等
提出变异性感知的量子比特分配与移动策略，规避高错误率量子比特和链路，将NISQ系统可靠性最高提升1.9倍。
Paulihedral：面向量子模拟内核的通用分块编译器优化框架
提出基于 Pauli 中间表示的分块编译框架 Paulihedral，深度优化量子模拟内核。
一个经过验证的量子电路优化器
提出首个用 Coq 完全验证的量子电路优化器 VOQC，基于深嵌入 SQIR 并证明优化正确性。
纯态量子比特量子计算的两个完备公理化
为纯态量子比特量子计算的 ZW 与 ZX 图示演算给出两个完备公理化。
时间最优的量子比特映射
提出一种理论上时间最优的 SWAP 插入方案，用于量子比特映射并给出可扩展启发式扩展。
量子计算平台中的缺陷：一项实证研究
首个对量子计算平台缺陷的大规模实证研究，揭示量子特有缺陷的分布、表现形式与反复出现的模式。
Muskit：面向量子软件测试的变异分析工具
提出 Muskit，一个对 Qiskit 量子程序进行变异分析、生成并执行变异体以评估测试用例的工具。
QDiff：量子软件栈的差分测试
提出面向量子软件栈的差分测试方法 QDiff，通过语义保持变换、电路过滤与分布等价检查发现关键缺陷。
面向纯量子比特量子力学的 ZX-Calculus 近极小公理化
提出两种 ZX-Calculus 完备公理化，规则近乎极小且具物理直观，并引入 ZX 图奇异值分解证明其充分性。
Bugs4Q：面向量子程序的真实缺陷基准
提出 Bugs4Q，一个含 36 个经人工验证的 Qiskit 真实缺陷及其复现测试用例的量子程序调试测试基准。
QMutPy：面向 Qiskit 量子算法与应用的变异测试工具
开发量子变异测试工具 QMutPy，为 Qiskit 量子程序提供量子门与测量变异算子并初步验证有效性。
面向高效超导量子处理器体系结构设计
提出面向应用的自动设计流程，在性能损失可忽略下生成简化的超导量子处理器体系结构。
通过脉冲与调度协同优化抑制量子计算机的 ZZ 串扰
提出脉冲与调度协同优化框架，可扩展地抑制超导量子比特 ZZ 串扰，无需特殊硬件。
合成量子电路优化器
提出 QUESO，按量子设备自动合成带高概率正确性保证的量子电路优化器。
Elivagar：面向分类的高效量子电路搜索
提出噪声引导的资源高效量子电路搜索框架 Élivágar，通过拓扑感知生成与廉价预测器加速 QML 分类电路设计。
带幽灵变量的量子 Hoare 逻辑
提出带幽灵变量的量子 Hoare 逻辑扩展，增强前后条件表达能力，并验证量子一次性密码本安全性。
量子电路的完备等式理论
首次提出并证明量子电路的完备等式理论，使两个电路表示同一酉映射当且仅当可由这些等式互相变换。