POPL（CCF A）（共 609 篇）
202692 篇 · 10(POPL)
贝叶斯分离逻辑：概率编程的逻辑基础与公理语义
提出贝叶斯分离逻辑 BaSL，为贝叶斯概率编程提供逻辑基础与公理语义，并支持贝叶斯更新等模块化推理。
ChopChop：一个对语言模型输出进行语义约束的可编程框架
提出首个可编程框架 ChopChop，通过对程序前缀的可实现性做共归纳分析，对语言模型生成施加语义约束。
贝叶斯程序分析引导的模糊测试
提出贝叶斯程序分析引导的目标导向灰盒模糊测试，通过可达目标预测与反馈更新提升漏洞发现能力。
通过自动循环向量化优化概率程序中的密度计算
提出可靠的自动循环向量化方法，用推测并行与不动点检查加速概率程序推断。
热带数学与λ演算 II：概率编程语言的热带几何
将热带几何用于高阶概率程序的统计推断，并设计交集类型系统组合式估计最可能运行。
具有向量化可编程推断的概率编程
提出 GenJAX 语言与编译器，将 vmap 向量化引入可编程概率推断，并证明其模型与推断操作向量化的正确性。
Nice to Meet You：合成实用的 MLIR 抽象转换器
提出 NiceToMeetYou 框架，无需 sketch 地合成 MLIR 中实用、可证可靠的整数抽象转换器。
基于 k-归纳的概率程序分段分析
提出基于 k-归纳的分段定量分析方法，为概率程序合成更紧的分段多项式界。
结果逻辑中的概率并发推理：独立性、条件化与不变式
提出 pcOL，首个能表达概率并发程序完整结果分布的程序逻辑，并支持几乎必然终止等推理。
有根基的多模态程序验证器
提出基于 Lean 的框架，用 monad transformer 代数自动导出可靠的验证条件生成器，以构建有根基的多模态程序验证器。
验证随机化分布式算法的几乎必然终止性
提出结合鞅与弱公平性的可靠证明规则，在 Caesar 上以 SMT 验证随机分布式共识的几乎必然终止。
面向抽象解释不精确性的逻辑
提出 Error Propagation Logic，用生成器从输入不精确性推导抽象解释结果误差上界。
兴趣分歧的模拟关系家族
提出 μdiv-模拟关系，统一强、弱、发散敏感等 12 种模拟，并在 Rocq 中形式化验证。
有界树宽、多上下文无关文法与向下闭包
证明 MSO 可定义的有界特殊树宽系统语言恰为多上下文无关语言，并用于计算向下闭包。
走向交互式定理证明器中纸笔风格的等式推理：基于等式饱和的方法
将定理解释为条件重写规则，用 e-graph 等式饱和在 Lean 中实现纸笔风格的等式推理 tactic。
编译到线性神经元
提出类型化高阶线性语言 Cajal，并证明其程序可编译为线性神经元，从而以可微方式直接编程神经网络。
Miri：面向 Rust 的实用未定义行为检测
提出 Miri，首个能发现确定性 Rust 程序中全部事实性未定义行为的动态检测工具。
抽象函数即类型：依赖类型论中成本与行为的模块化验证
在单价依赖类型论中把抽象函数编码为类型，用相位区分与密封效应支持成本与行为的模块化验证。
面向 effect handlers 的关系分离逻辑
提出首个面向 effect handlers 的关系分离逻辑 blaze，支持在含可变状态与并发的程序中证明程序间关系性质。
为量子比特映射与路由生成编译器
提出设备状态机抽象与DSL，可自动为任意量子处理器生成量子比特映射与路由编译器。
ArchSem：可复用的宽松架构严格语义
提出架构通用框架 ArchSem，模块化组合 ISA 与并发模型，并在 Rocq/Isabelle 中实例化 Arm/RISC-V 以支持严格验证。
基于关系式 NetKAT 的网络变更验证
提出 Relational NetKAT 规格语言与转换器/自动机算法，以验证网络变更是否符合意图。
消息传递并发测试的复杂度
系统刻画通道式消息传递并发一致性测试的复杂度版图，给出近最优算法与实验验证。
DafnyMPI：一个用于验证消息传递并发程序的 Dafny 库
提出 DafnyMPI 库，使 Dafny 能验证 MPI 程序的无死锁、终止与功能等价。
通过子结构依赖追踪进行安全推理
提出基于输出约束的子结构类型框架，统一刻画能力、定量信息泄漏、沙箱与授权协议等安全特性，并以单一逻辑关系证明其安全性。
面向 GPU Warp 级并行的模块化静态代价分析
提出首个可精确处理线程分歧的 GPU warp 级并行关系代价静态分析，支持资源度量与代价关系参数化，并实现 Rocq 验证工具 Pico。
参数化无限状态反应式合成
提出反例引导的参数化无限状态反应式合成方法，可生成可实例化并带不变式/秩函数证明的系统。
轨道闭包与矩阵群的判定问题
给出判定一个簇是否为 s-生成交换代数矩阵群作用下点轨道闭包的多项式空间算法。
Coco：组合式异构生产性的余递归
提出 CHP 框架与 Rocq 库 Coco，通过组合式异构生产性自动化支持广泛余递归定义。
一种基于补运算的错误性类型化方法
提出以正规形集合为类型语义、带补运算的双侧类型系统，可同时验证函数式程序的正确性与错误性。
去芜存菁：理解带归纳定义的分离逻辑证明机制的（不）完备性
引入弱分离逻辑 WSL 刻画 SLID 证明机制的不完备性，将证明失败归因于非标准模型，并通过 FOL 归约自动寻找反模型。
增量计算中的有状态差分算子
提出有状态差分算子的形式规约，在 Rocq 中机械化验证，可指导新算子设计并刻画 join 与 Datalog 聚合等既有算子。
通过优化领域特定语言加速语法引导的程序合成
提出 AMaze 框架，自动优化 DSL 以加速语法引导程序合成，最高取得 4.35× 加速。
用于局部敏感性分析的依赖余效应
提出 Local Fuzz：带依赖余效应的类型系统，刻画程序局部敏感性，给出优于 Fuzz 的差分隐私保证。
既要编码又要吃到蛋糕：在类型论中局部地控制计算
提出 LRTT 类型理论，以局部抽象封装用户自定义计算规则，并给出保守性证明与 Rocq 原型。
一人为大家，大家为一人：利用并行程序内部确定性的程序逻辑
提出利用内部确定性简化并行程序验证的程序逻辑，并在 Rocq/Iris 中机器化验证。
U-Turn：通过反转方向增强不正确性分析
提出 U-Turn，将不正确性逻辑与充分不正确性逻辑结合，复用前者启发式指导后者，增强错误分析。
ChiSA：面向轻量级 Chisel 验证的静态分析
提出 Chisel 静态分析形式基础与硬件值流分析方法，并实现首个 Chisel 静态分析器 ChiSA，支持轻量级验证。
线性逻辑视角下的 JAX Autodiff
将 JAX Autodiff 编码到线性 λ-演算，证明定性与定量可靠性，并说明 unzipping 可选。
几乎可交换迁移系统的上下文无关语言可达性
将 CFL 可达性推广到几乎可交换迁移系统，证明其同态像半线性并给出多项式时间 Presburger 构造。
通过元分析引导的洞填充进行归纳程序合成
提出用抽象解释元分析预测最佳洞填充顺序，以提升归纳程序合成中自上而下搜索效率。
JavaScript 正则表达式的形式化验证：一个已验证的机器化语义及其应用
首个经机器化验证、忠实于 ECMAScript 规范的回溯正则语义，并用于重写等价与 PikeVM 证明。
面向自底向上枚举式合成的定向度量（Oriented Metrics）
提出 oriented metric 结构统一搜索空间缩减技术，实现度量通用的自底向上合成器，性能提升逾一个数量级。
帝国的幽灵：从基于交错的证明中提取模块化
将并发程序基于交错的正确性证明自动转换为 Owicki-Gries 风格线程模块化证明，并合成 ghost 变量以压缩证明。
Zoo：使用分离逻辑验证并发 OCaml 5 程序的框架
提出 Zoo 框架，在 Rocq 中借助 Iris 分离逻辑验证 OCaml 5 细粒度并发算法，并验证了标准库与 Saturn/Eio 中的数据结构。
多方会话类型的合成式重构
提出合成式多方会话类型方法，直接以全局协议LTS检查进程，无需投影与局部类型，兼具表达力与组合性。
参数化量子电路的验证
首个全自动验证参数化量子程序关系性质的框架，以同步加权树自动机刻画无限族量子态并给出判定过程。
量子电路只是一个相位
提出仅用相位操作与 if-let 式子空间选择的量子编程原语，并给出范畴语义与可靠编译器。
一等宇宙层级的规范化
证明 Agda 风格一等宇宙层级理论的规范化、等式与类型检查可判定性，并证明层级原语可安全擦除。
面向量子程序的一种富有表达力的断言语言
提出以广义Pauli算子准概率分布表示量子谓词的断言语言，可表达含循环量子程序的最弱前置条件，并建立可靠且相对完备的量子Hoare逻辑。
RapunSL：以分离、线性组合与混合理清量子计算
提出量子分离逻辑 RapunSL，引入线性组合与混合连接词，将叠加态与混合态推理归约为纯态推理。
行与能力作为模态效应
提出统一框架，用模态效应类型编码并比较基于行多态与基于能力的效应系统，证明编码保持类型与语义。
通过代数效应对动态线程的等式公理化：有限关系上的预层、带标号偏序集与参数化代数理论
用参数化代数理论给出 fork/wait 动态线程的完备等式公理，并构造一阶全抽象的并发达标语义。
使用投影 Clifford 的 qudit 量子编程
提出面向 qudit 的投影 Clifford 类型系统与 λPc 演算，经 Curry-Howard 对应编译为量子电路。
索引归纳-递归（IIR）类型的典范性
为支持可数宇宙层级与索引归纳-递归（IIR）类型的 Martin-Löf 类型论证明典范性，并给出将 IIR 归约到 IR 的构造。
局部上下文类型推断
提出基于上下文类型论的局部上下文类型推断，为 System F 的 LTI 给出首个机械化形式化与算法设计。
带满射配对的算法转换：一种语法且无类型的方法
通过语法方法恢复满射配对下类型转换的可判定性，并用 Rocq 机械化验证。
用于证明公理内存一致性模型下公平非终止的重现集
将序列程序的重现集推广到弱内存并发程序，给出公平非终止的可靠且多模型完备的证明与自动检测技术。
处理作用域检查：动态作用域外泄检查的比较框架
首次形式化研究动态作用域外泄检查，提出并验证 Cause-for-Concern 检查，并与静态环境分类器比较表达力。
Cryptis：分离逻辑中的密码学推理
将符号密码学推理嵌入 Iris 分离逻辑，提出认证协议新规约，使协议验证结果可复用于更大系统。
论电路描述语言、索引单子与资源分析
为 Proto-Quipper 演算提出基于单子的指称模型，分离值与电路副作用，并支持电路资源分析。
相对单子元语言
将单子元语言推广到相对单子设置，给出完备语义，并据此重新刻画 graded monads 与 arrows 并设计保守扩展语言。
刻画可不相交组合的理论集合
通过 Galois 连接刻画可与给定可判定理论集合不相交组合的最大理论类，并否证若干开放问题。
TypeDis：一个面向 disentanglement 的类型系统
提出类型系统 TypeDis，用带时间戳的区域类型自动验证并行程序的 disentanglement，免去手工逻辑证明。
Hadamard-Pi：等式量子编程
通过给经典可逆语言Π添加Hadamard原语，建立量子编程语言的可靠完备等式范畴语义，并给出正交矩阵群的有限呈现与合成算法。
正则语言中的迹计数与采样
研究正则语言中 Mazurkiewicz 迹的计数与近似均匀采样，给出 #P 复杂度结果及 FPRAS/FPAUS 算法。
Boolean-kinded 类型系统中的 let 泛化、多态递归与变量最小化
为 Boolean-kinded Hindley-Milner 扩展给出等式泛化与半统一算法，支持 let 泛化和多态递归，并最小化布尔类型变量。
布尔代数子类型的简单本质：代数并、交、否定与等递归类型的语义可靠性
用五族特征布尔同态刻画布尔代数子类型，给出语义可靠性、判定过程与 co-NP 硬度。
支持特设多态的可扩展数据类型
提出结合行类型/行多态与类型类特设多态的可扩展数据类型语言设计，并给出机器化验证的可靠性证明。
面向 RDMA 的经过验证的高性能可组合对象库
提出经形式化验证的 RDMA 多节点可组合对象库 LOCO，并给出内存模型无关的模块化验证框架 Mowgli。
一个惰性并发的可转换性检查器
提出一种依赖惰性与并发的可转换性检查算法，总能找到存在的简单解，避免启发式带来的冗余计算。
Big-Stop 语义：在大步判断中实现小步语义
提出 big-stop 语义，用归纳定义的大步求值判断等价刻画小步闭包，可表达发散且无需错误状态。
用判断性 Monad 律处理高阶效应操作
提出支持高阶效应操作处理器的核心演算，处理器由无律原始 Monad 承载而计算判断满足判断性 Monad 律，并给出语义模型与元定理。
函数逻辑编程的域论语义
基于 call-by-push-value 重构函数逻辑编程核心演算，并以 lower powerdomain 给出与抽象机完全抽象的域论语义。
核心函数式语言的惰性线性
提出 Linear Core，将线性资源语义从语法出现扩展到惰性求值语义，并证明其可靠性及优化保持线性。
严格性的类型化
提出更精细的严格性定义，并在按名调用与 CBPV 中建立类型系统，证明其准确刻画变量的运行时使用。
Intel-x86 程序的参数化验证
证明无界线程数下 k-alternation 有界 eTSO 参数化可达性可判定，并首次用 BQO 良结构系统验证无限状态程序。
被语言危及，被编译器拯救：通过语义反向翻译实现鲁棒安全
借助 Reckon 分离逻辑与语义反向翻译，将类 C 程序编译到 capability 机器，保证鲁棒安全。
具有连续计数器的系统的一般可判定性结果
证明连续计数器系统到达目标配置的指令序列语言为正则，从而为多类无限状态系统保持可达性可判定。
Di- 即 Directed：经由双自然性的一阶有向类型论
提出一阶有向类型论，以范畴与双自然变换解释有向相等，并借助双自然性刻画 J 规则与 (co)end 量词。
从语义到句法：一种面向 comprehension 范畴的类型论
提出一种内化类型间态射、含 Π/Σ/同一类型的类型论，并证明其在 comprehension 范畴语义下的可靠性。
AdapTT：依赖类型转换的函子性
提出 AdapTT 类型理论，以适配器抽象刻画类型构造子的函子性，并推导归纳类型转换的结构法则。
无仲裁一致性是可用的（反之亦然）
提出统一语义框架，证明对象规格可无协调实现当且仅当无仲裁，统一并推广 CAP 类结果。
通过纤维化的高阶行为一致性
提出统一范畴方法，用高阶抽象规范与纤维化证明最大行为（双）一致性构成同余。
经典计算概念与 Hasegawa-Thielecke 定理
为经典逻辑的线性 L-演算建立对话 duploid 语义，并据此证明 Hasegawa-Thielecke 定理。
超函数（Hyperfunctions）：通信延续
识别多种算法中隐藏的 hyperfunction 共同模式，建立统一框架，并用于 CCS 全抽象语义与 Haskell 协程库。
可扩展微服务的一致性更新
提出微服务混合模式更新的形式化框架与保证一致性的算法，并证明忽略语义的方法必然导致不一致。
什么是 monoid？
通过左斜与双斜多范畴统一 monoid 概念，涵盖相对单子与 call-by-push-value 等例子。
带消去约束的有界排序多态
为 sort 多态引入带界的 sort 变量与消去约束，恢复多排序类型论的表达力与主类型推断。
商多态
提出 choice polymorphism，使函数可复用于不同商类型，避免代码重复并接受更多合法定义。
更正：Unrealizability Logic
澄清原文健全性陈述中的隐含假设，并修正其完备性证明中的缺陷。
Welterweight Go：装箱、结构子类型与泛型
提出 Go 核心模型 WG 与运行时低级语言 LWG，给出兼顾结构子类型与泛型的类型导向编译方案。
202579 篇 · 9(POPL)
带循环的离散概率程序后验分布的保证界
提出残差质量语义与几何界语义，为带循环离散概率程序的后验分布自动计算保证上下界。
自动化程序精化：用精化演算引导并验证代码大语言模型
提出 Refine4LLM，用精化演算自动引导并验证 LLM 生成代码，在保证正确性的同时提升自动化程度。
TensorRight：张量图重写的自动验证
提出首个可验证任意秩与尺寸张量图重写正确性的自动验证系统 TensorRight。
混合粒子滤波的推断计划
提出推断计划接口与 Siren 语言，让开发者控制混合粒子滤波的变量划分，并用抽象解释静态分析判定其可满足性。
BlueBell：关系提升与独立性的联盟及其在概率推理中的应用
提出概率程序逻辑 BlueBell，以“联合条件化”模态统一一元式与关系式概率推理。
概率终止的可靠且完备证明规则
为带离散概率选择与有界恶魔非确定性的命令式程序，给出算术断言语言中可靠且相对完备的定性/定量概率终止证明规则。
一种定量概率关系霍尔逻辑
提出定量概率关系霍尔逻辑 eRHL，克服 pRHL/apRHL 的随机对齐限制，并给出可靠性与完备性结果。
模式化数据竞争自由
扩展 OCaml 类型系统，以 mode 保证多线程数据竞争自由并兼容顺序代码。
CF-GKAT：控制流变换的高效验证
提出 CF-GKAT，扩展 GKAT 以支持非局部控制流和硬编码值，高效可靠完备地验证控制流变换的迹等价。
基于多重上下文无关语言可达性的程序分析
提出多重上下文无关语言可达性模型，以可调精度、可判定地近似交错 Dyck 可达性，并给出算法复杂度与实现评估。
Axe ’Em：用归纳公理消除伪状态
提出基于归纳公理的可靠精化方法，弥合一阶抽象与良基/有限域语义间的鸿沟，消除伪状态。
泛型精化类型（Generic Refinement Types）
提出泛型精化类型，用 ghost 参数抽象函数契约不变量，保持 SMT 可判定验证并在 Rust 中实现。
程序验证算法的原始-对偶视角
提出统一的原始-对偶框架，用广义Lagrangian刻画并设计验证算法，推导已有方法并给出新的不动点逻辑判定算法。
不相等/相等图（Dis/Equality Graphs）
首次形式化直接支持不等式的 e-graph，证明其比等式嵌入编码更高效，并在 egg 中实现验证。
MimIR：面向 DSL 时代的可扩展且类型安全的中间表示
提出以纯类型系统为核心的可扩展高阶中间表示 MimIR，让开发者以插件形式声明并优化领域特定操作。
高阶概率程序的近似关系推理
提出 Approxis：面向高阶概率程序近似等价的关系分离逻辑，支持误差信用与逻辑关系，并在 Coq/Iris 中机器化验证多个案例。
编译对推测性常量时间（speculative constant-time）的保持
揭示主流编译器不保持推测性常量时间，并给出经 Coq 验证保持该性质的编译器原型与类型检查器修补方案。
面向随机非确定性的 Demonic Outcome Logic
提出 Demonic Outcome Logic，统一推理同时含随机选择与恶魔非确定性的程序，并支持循环终止与结果分布量化。
量子电路描述语言中灵活的基于类型的资源估计
为 Quipper 设计基于效应与细化类型的类型系统，自动推导电路宽度、深度、门数等资源上界。
面向量子程序优化的线性与非线性关系分析
将相位折叠重铸为仿射关系分析，借助经典关系域把优化扩展到含复杂控制流的量子程序。
RE#：基于导数的高性能正则表达式匹配，支持交、补与受限环视
提出无回溯的正则匹配工具 RE#，基于符号导数支持交、补与受限环视，匹配复杂度对输入线性。
自动化 Dirac 记号中的等式证明
证明 Dirac 记号的一阶理论可判定，并用项重写高效判定等式，实现等价性检查器。
SNIP：编译器变换中的推测执行与非干扰保持
提出基于新型模拟关系的证明方法，统一保证编译器变换在推测语义下保持非干扰，并修复寄存器分配引入的安全缺陷。
支持内涵分析的元编程依赖类型理论
提出 DeLaM 分层模态依赖类型理论，支持开放代码的引用、组合、递归分析与类型安全代码生成。
通过抽象解释计算式地设计超逻辑
提出基于抽象解释的通用计算式框架，设计并推导证明程序超属性的多种超逻辑及其证明规则。
Fulminate：在 C 中测试 CN 分离逻辑规约
提出 Fulminate，将带 CN 分离逻辑前后条件的 C 代码翻译为运行时检查代码，实现所有权测试。
QuickSub：高效的同构递归子类型判定
提出高效易实现的同构递归子类型算法 QuickSub，最坏复杂度 O(nm)，常见情况近线性，并用 Coq 形式化验证。
程序逻辑 à la carte
通过组合可复用的程序逻辑片段，实现跨语言及语言内模块化定义并证明程序逻辑。
符号自动机：模理论下的 ω-正则性
将符号自动机从有限字推广到 ω-正则语言，统一交替/非确定 Büchi 自动机与 LTL、PSL 的模理论框架。
面向定时消息传递协议的语义逻辑关系
提出完全语义的逻辑关系，用于验证异构应用与硬件设备对定时消息传递协议的合规性，并配以 refinement 类型系统与 Rust 类型检查器。
论简单类型 lambda 演算的可判定与不可判定扩展
给出 finitary PCF 四种扩展不可判定性的简单证明，并用类型系统刻画含引用单元的可判定片段。
用三维精化代数统一组合式验证与认证编译
提出三维精化代数及其组合语义框架，并在 Coq 中统一组合式验证与认证编译。
组合式不精确概率：分级单子与 Markov 范畴的解决方案
用命名不确定选择与分级单子，在 Markov 范畴中为不精确概率给出全组合语义，并获得更紧界。
用于高效 WebAssembly 机器化的 Progressful 解释器
提出 progressful 解释器，用 Coq 依赖类型认证健全性与 progress，高效扩展 Wasm 2.0 机器化。
导数引导的符号执行
提出符号导数引导的符号执行，借助 LTLf 规约与符号自动机剪枝，高效证伪带不透明库的程序中数据结构安全性质。
混合大小访问的 C/C++ 模型检测
提出 Mixer——面向混合大小访问程序的最优 DPOR 算法，并在 GenMC 中实现，首次自动验证此类 C/C++ 并发代码。
Hoare 式逻辑的分类学：基于谓词变换器与带顶和测试的 Kleene 代数走向整体视角
通过谓词变换器和 TopKAT 建立类 Hoare 逻辑的分类学，并给出 Lisbon 逻辑的新 TopKAT 刻画。
Archmage 与 CompCertCast：支持整数-指针转换的端到端验证
提出 Archmage 内存模型框架及 CompCertCast 编译链与源级逻辑，首次实现含整数-指针转换程序的实用端到端验证。
在守卫类型论中建模递归与概率选择
在守卫类型论中为带概率选择与递归类型的 FPC⊕ 建立操作与指称语义，并支持充分性与上下文等价推理。
最佳抽象解释
研究程序何时在给定抽象域上达到最佳抽象解释，证明其不可计算与难以达成，并提出证明最佳性的程序逻辑。
通过函子、同态与模通用地自动化分离逻辑
提出基于函子、同态与环上模的抽象代数理论，通用自动化分离逻辑，并自动实例化数据结构推理器。
使用层级同步树自动机验证量子电路
提出层级同步树自动机（LSTA）表示量子态集，实现可扩展且支持参数化的量子电路验证。
Affect：一种仿射类型与效应系统
提出 Affect：用仿射类型与效应静态追踪续延的 one-shot/multi-shot 用法，并在 Coq/Iris 中证明其可靠性。
时序超活性的余归纳证明
提出 HyCo：面向 ∀*∃* 安全型时序超性质的余归纳证明框架，并在 Coq 中机械化与验证其可靠性。
用于高效无限状态反应式合成的时序逻辑翻译
提出首个在公式层融合一阶与时序推理的监控器构造，将无限状态时序规约翻译为语义增强的符号博弈以加速反应式合成。
Coq 与 C 之间经过验证的外部函数接口
提出 VeriFFI，在 Coq 与 C 之间建立可验证的 FFI，保证组合程序的类型安全与正确性。
Do You Even Lift? 强化编译器针对 Spectre 攻击的安全保证
提出安全编译 lifting 框架，将 Spectre 防御的安全保证从弱推测语义提升到强推测语义，无需新证明。
依赖不可区分演算的一致性
确定 DCOI_ω 实例，并证明该依赖不可区分演算逻辑一致、规范化且类型转换可判定。
自上而下还是自下而上？同步多参与方会话类型的复杂度分析
系统比较多参与方会话类型的自顶向下与自底向上工作流，建立类型图算法并给出子类型、投影、推理与性质检查的复杂度。
简单线性循环：代数不变量与应用
提出多项式空间算法，为简单线性循环计算最强代数不变量，并给出验证与合成的复杂度结果。
你们的所有基础都属于我们：证明助手中的 Sort 多态
为证明助手提出 sort 多态及其元理论，并在 Coq 中实现，解决跨种类定义复用与扩展问题。
翻译式分离逻辑验证器的形式化基础
提出核心 IVL 形式化框架，统一翻译式分离逻辑验证器的前端翻译与后端验证，并在 Isabelle/HOL 中机化。
带有交集与并集类型的双向高阶多态
提出带显式类型应用、交集与并集类型的双向高阶多态类型推断，给出可靠、完备、可判定算法并在 Coq 中形式化。
确定性计算的代数本质上是不可完备的
证明 KAT 的确定性片段不能由任何有限个正则控制流操作生成。
在 ML 模块中用 Zipper 避免签名规避
提出 ZipML，以浮动字段和签名 zipper 消除 ML 模块的签名规避问题，并证明类型系统可靠。
Grove：双向类型化的协作结构编辑器演算
提出 Grove 协作结构编辑器演算，消除 patch 合成与三方合并，使编辑可交换并显式表示冲突，同时提供双向类型化支持。
域名系统（DNS）的可达性分析
首次给出 DNS 验证问题的判定过程，证明其复杂度为 2ExpTime，并将其归约到下推系统验证。
Barendregt 与 Knaster 和 Tarski 相聚：面向带绑定语法的强规则归纳
为带绑定语法和规则系统提出通用强规则归纳准则，支持 Barendregt 变量约定并覆盖无穷语法。
RELINCHE：在宽松内存一致性下自动检查线性一致性
提出 Relinche，全自动模型检测器，在弱内存一致性下验证并发库的原子性与功能正确性。
Tail Modulo Cons、OCaml 与关系分离逻辑
在 OCaml 编译器中实现 tail modulo cons 变换，并用 Coq/Iris 机器化证明其正确性。
Biparsers：面向数据同步的精确打印
提出首个支持非单射解析器精确打印的 biparser 框架，用 lens 统一解析与打印，并实现 JSON/YAML 子集。
交互等价
提出交互等价：只计项与上下文的交互步数，证明它是等式理论并刻画为Böhm树等价B。
代数程序分析的增量算法
提出增量代数程序分析算法，通过树表示路径表达式并增量更新解释结果，显著加速分析。
Call-by-Push-Value 的抽象操作语义方法
基于预层范畴与高阶抽象 GSOS，为 CBPV 和细粒度 CBV 建立模块化的程序等价推理方法。
论扩展 Incorrectness Logic 以支持反向推理
通过欠指定扩展 Incorrectness Logic，使其支持反向推理，并证明可靠性与部分完备性，且在 Isabelle/HOL 中形式化。
用余归纳形式化图算法
提出以余归纳结构为起点的图与图算法形式化理论，并在 Agda 中实现可复用技术。
Qurts：通过带生命周期的仿射类型进行自动量子反计算
提出 Qurts，用带生命周期的仿射类型统一实现量子程序自动反计算。
有限选择逻辑编程
提出有限选择逻辑编程，用选择代替否定表达多解，并实现 Dusa 求解器。
VeriRT：面向实时分布式系统的端到端验证框架
提出端到端形式化验证框架 VeriRT，弥合实时分布式系统高层计时抽象规约与底层汇编实现之间的形式鸿沟，并在 Coq 中机器化验证。
代数时序效应：递归类型高阶程序的时序验证
提出代数时序效应，用 later 模态处理递归类型，为高阶程序提供可证明安全性与活性的时序效应系统。
再执行式宽松内存并发模型
提出再执行式内存模型 XMM，以近似每执行的语义统一解释宽松并发，并实例化为 XC20。
使用合成守卫域理论的渐进类型指称语义
提出基于合成守卫域理论的渐进类型指称语义，统一证明βη等式有效性与渐进性定理。
多面体归约的最大化简化
提出分段简化方法，利用所有可用重用，使多面体归约达到最小渐近复杂度。
BiSikkel：Agda 中的多模态逻辑框架
在 Agda 的 Sikkel 库上实现多模态逻辑框架 µLF，支持对多模态程序进行证明并抽取到元语言。
Pantograph：一种流畅且带类型的结构编辑器
提出 Pantograph 结构编辑方案，用类型化一洞上下文与类型差分，在保持程序良构的同时实现流畅编辑。
正则一阶理论的判定问题
研究正则一阶理论的判定问题，证明 EPR 与 Gurevich 类在经典设定下可判定但在正则理论下不可判定，并给出可判定子类。
Flo：渐进式流处理的语义基础
提出参数化流语言 Flo，形式化 streaming progress 与 eager execution，统一流处理语义基础。
λ-抽象的对偶性
通过共指数与共抽象为 λ-抽象建立对偶，统一控制效应语义并导出经典控制算子。
Löb 归纳的模态解构
用模态类型论分解 Löb 归纳，提出捕获 topos of trees 模态结构且不排除 canonicity/normalization 的 guarded 类型论 Gatsby。
202493 篇 · 8(POPL)
基于矩匹配高斯混合的概率程序推断
提出高斯语义，用矩匹配高斯混合逼近概率程序语义，并证明通用逼近定理与二阶矩算法 SOGA。
基于动态双向 Dyck 可达性的即时静态分析
提出每次更新 O(n·α(n)) 的动态双向 Dyck 可达性算法，用于即时静态分析并实现千倍加速。
正几乎必然终止：复杂度与证明规则
证明概率程序的PAST复杂度为Π^1_1完全，并给出基于超限序数的可靠完备证明规则。
ReLU 凸包近似
提出快速精确的 ReLU 凸包过近似方法 WraLU，用更少约束实现更紧近似并集成到神经网络验证器 PRIMA。
强不变式很难：论（概率）程序最强多项式不变式的困难性
证明单路径多项式循环的最强多项式不变式计算至少与 Skolem 问题同难，并推广到概率程序的矩不变式。
高阶分离逻辑中的异步概率耦合
提出支持异步概率耦合的高阶概率关系分离逻辑 Clutch，并用于证明高阶程序的上下文精化与等价。
通过加速求解无限状态博弈
提出首个带加速技术的无限状态博弈符号半算法，避免传统不动点求解发散并提升求解能力。
可解多项式理想：程序分析中的理想反射
将任意循环抽象为可解多项式映射模型，从而把循环多项式不变式生成技术推广到一般程序。
面向长时程机器人任务的示教编程
提出面向长时程机器人任务的程序化示教学习算法，先学程序草图，再用 LLM 引导搜索补全并判定不可实现性。
位向量操作语法引导合成的增强枚举技术
融合项图枚举、示例过滤、LLM 优先级与自底向上推导，提升位向量语法引导合成性能。
Flan：面向程序分析的高表达力高效 Datalog 编译器
提出嵌入 Scala 的 Datalog 编译器 Flan，用多阶段编程生成专用代码，兼顾表达力与性能。
数学库函数的实现与合成
提出 MegaLibm，一个用于实现、测试、调优与合成数学库函数的领域特定语言。
基于符号执行的可靠渐进验证
为基于符号执行的渐进验证给出形式化与可靠性证明，并发现修复实现中的可靠性缺陷。
基于抽象解释的最优程序合成
提出基于抽象解释与A*搜索的最优程序合成框架，可证明最优并剪枝次优子树，提升可扩展性。
带公理的正交逻辑
为带公理的正交逻辑建立证明论，给出广义切消、三次时间判定算法及其与有界宽度消解和 Datalog 扩展的关系。
高阶贝叶斯网络，精确地
提出高阶 λ-演算，可编译为贝叶斯网络，并给出精确、组合且考虑代价的语义。
有限草堆中的无限针：在演绎验证中寻找无限反模型
提出符号结构与模型发现过程，为演绎验证中仅有无穷模型的量词公式找到有限表示的反模型。
单调性与程序分析的精度
刻画程序单调性与抽象解释完备性之间的关系，给出可被精确分析的单调程序片段。
带时间信用的分离逻辑中的 thunk 与 debit
在 Iris 时间信用分离逻辑中机器化重建 Okasaki 的 thunk/debit 摊还推理规则，并验证流与多种队列。
一个用于验证 CompCert C 程序的 Iris 实例
在 Iris 中构建基于 CompCert 语义的分离逻辑实例，以验证 C 程序正确性。
基于洞的完全类型错误定位与恢复
提出标记 lambda 演算，首次形式化完全类型错误定位与恢复，并在 Hazel 中实现无无意义编辑器状态的实时环境。
无死锁分离逻辑：线性性为依赖高阶消息传递带来进展
提出线性并发分离逻辑 LinearActris，用线性性保证依赖高阶消息传递程序无死锁且无泄漏。
面向模式正则语言的预测性运行时监控
提出面向模式正则语言的预测性运行时监控，能在并发执行重排序中暴露高层时序违规，并给出常空间流式线性时间算法。
通过抽象解释对【不】正确性转换式程序逻辑的计算式设计
用抽象解释统一刻画正确性与不正确性转换式程序逻辑，并给出构造可靠完备证明系统的计算式方法。
VST-A：一个基础可靠的注解验证器
提出 VST-A，一个基于 VST 丰富断言语言和 Coq 可靠证明的注解验证器，可将 C 函数验证归约为直线 Hoare 三元组。
Decalf：一个有向、带效应且成本感知的逻辑框架
提出 Decalf，用内在前序刻画带效应函数式程序成本界的有向成本感知逻辑框架，并给出单纯集模型。
程序化策略合成：消解概率程序中的非确定性
提出基于最弱前置条件的演绎框架，半自动地为含随机与纯非确定的命令式程序合成无记忆确定性策略，使其满足期望界等定量规约。
完全可组合且充分的验证编译：开放模块间的直接精化
提出无需编译器内部假设的开放模块组合式验证编译，用Kripke内存关系建立直接精化并保证组合性与充分性。
论高阶效应程序的模型检测
将高阶代数效应程序归约为高阶递归方案，并刻画效应处理器下模型检测的可判定边界。
递归量子酉程序合成的可行性论证
提出首个量子酉程序合成框架 QSynth，借助 SMT 求解自动合成递归定义的量子酉电路。
在 Coq 中形式化 Core Why3
在 Coq 中为 Why3 逻辑片段建立形式语义，并机器化验证其证明系统与变换的可靠性。
弱内存测试有多难？
证明多种弱内存模型下一致性测试在参数有界时仍 NP 完全，并与 SC、x86-TSO、PSO、Relaxed 形成计算分离。
引导式等式饱和
提出引导式等式饱和，将复杂重写拆成经人工中间引导连接的自动等式饱和步骤，提升可扩展性。
生成非“无用”的良类型项
提出一种非局部生成算法，生成会使用参数的良类型函数，显著提升编译器随机测试效率。
高效 CHAD
用稀疏向量、状态传递和去函数化优化 CHAD，使反向模式自动微分达到预期复杂度，并给出 Agda 复杂度证明。
判定递归程序的异步超属性
提出一种表达力更强的异步超属性逻辑，并在有限状态与下推模型上研究其模型检测复杂度。
良括号控制流的逻辑本质
提出首个基于分离逻辑的 Hoare 式程序逻辑，用于推理良括号控制流，并在 Coq/Iris 中机械化。
无需区间的内部参数性
提出一种无需显式区间或高维立方语法的内部参数性类型论，并以预层与胶合模型证明外部参数性与 canonicity。
面向静态安全 WebAssembly 的索引类型
提出 Wasm-precheck，用索引类型静态检查程序值约束，从而安全移除 Wasm 的动态安全检查。
检查无限下降的复杂性景观
在逻辑无关的抽象框架下，系统刻画循环证明无限下降检查准则的参数化复杂度，并提出改进算法。
鲁棒可达性约束的推断
用理论无关溯因推断不可控输入约束，扩展鲁棒可达性以刻画大部分可复现的程序违反。
符号化的 Parikh 定理
为符号自动机与文法提出多项式时间构造，将 Parikh 计数抽象编码为存在 Presburger 公式，避免指数爆炸。
随机图的概率编程接口：马尔可夫范畴、graphon 与名义集合
建立图上概率编程语义与 graphon 的对应，并给出三种构造证明每个 graphon 均可由等式理论产生。
非良类型程序不会求值
提出双侧类型系统，可反驳类型公式，从而保证良类型程序不出错、非良类型程序不会求值。
代数效应在 Cubical Agda 中遇上 Hoare 逻辑
在 Cubical Agda 中用商类型形式化带方程的代数效应，并提供效应通用的 Hoare 逻辑与等式推理。
Cubical Agda 的内部参数性与观察式参数性
提出首个实用的内部参数性证明助手 Agda--bridges，并基于 SRP 给出内部自由定理的单行证明。
Shoggoth：策略重写的形式化基础
提出 Shoggoth，为策略重写建立指称语义与基于位置的弱前置条件演算，并在 Isabelle/HOL 中机化验证。
流水线及其之外：面向带 future 的代数数据类型的图类型
提出支持 future 与递归数据类型近乎任意组合的图类型系统，可静态推断并证明可靠性。
现代 JSON Schema 的验证：形式化与复杂度
首次形式化现代 JSON Schema，并证明其数据验证问题是 PSPACE 完全，根源在动态引用。
带环视断言的正则表达式的高效匹配
提出带环视断言正则表达式的形式语义和 O(m·n) 匹配算法，并用 oracle-NFA 实现，避免回溯导致的超线性时间。
API 驱动的程序合成：面向静态类型检查实现的测试
提出 API 驱动的程序合成方法，复用已有库 API 生成小型良类型程序，以检测静态类型检查实现中的缺陷。
SimuQ：面向模拟编译的量子哈密顿量模拟编程框架
首个支持哈密顿量级编程与脉冲级编译到异构模拟量子模拟器的框架。
Trillium：面向内涵精化的高阶并发与分布式分离逻辑
提出 Trillium 分离逻辑框架，以内涵精化证明高阶并发与分布式程序的安全和活性性质。
抽象数据类型的语义代码重构
提出基于CEGIS的自动化语义重构方法，为ADT数据表示变更生成语义等价的实现。
基于守卫交互树的效果模块化指称语义
提出守卫交互树及其分离逻辑，用于在 Coq 中模块化地给出带高阶效应的语言指称语义并证明类型安全。
Dolev-Yao 超属性的判定与复杂度
首次提出在有限会话与子项收敛等式理论下判定 Dolev-Yao 超属性的过程，并分析若干片段的复杂度。
基于秩函数的分布式协议活性性质的大部分自动化验证
提出 LVR，首个可大部分自动验证分布式协议活性性质的框架，将活性归约为秩函数与无死锁的安全性验证。
当子类型约束带来自由：面向一等多态的新颖类型推断方法
提出基于多界多态的子类型类型推断系统 F≤ 与算法 SuperF，显著提升一等多态的类型推断能力。
面向动态语言的多态类型推断
提出结合多态、交并类型与子类型的类型系统，并给出可靠且终止的类型重建算法，适用于动态语言。
交换性简化参数化程序的证明
提出参数化程序的交换性归约族，使归约后的程序可用更简单的幽灵变量证明，从而更易自动验证。
基于 barb 与上下文的量子双相似性：限制非确定性观察者的能力
提出线性量子进程演算 lqCCS，并细化操作语义以约束上下文，给出更符合量子理论的 barb 与上下文双相似性。
一种通用、可靠且完备的前向推理技术：面向机器验证的线性一致性证明
提出通用、可靠且完备的前向推理证明方法，并在 TLAPS 中机器验证若干并发对象的线性一致性。
面向因果并发的更粗等价关系
提出比迹等价更粗的 grain 等价，并给出判定因果并发性的常数空间流式算法。
可靠地处理线性
提出控制流线性，使线性类型与多次调用效应处理器可靠结合，形式化验证并修复 Links 缺陷。
答案精化修改：面向代数效应与处理程序的精化类型系统
提出答案精化修改（ARM）精化类型系统，可靠验证代数效应与处理程序。
精化类型的机器化
提出精化演算 λRF，证明语义子类型与参数多态结合的类型系统可靠性，并在 Liquid Haskell 与 Coq 中机器化元理论。
自动并行管理
通过编译器把潜在并行性嵌入调用栈、运行时按需转为并行任务，自动管理并行性并保持 work/span 渐近性质。
论多项式递归程序的学习
引入 P-finite 自动机，并证明其可在 Angluin 的 MAT 精确学习模型中多项式时间学习。
广义代数数据类型（GADTs）的本质
在带递归类型和内部化类型等式的 System Fω 扩展中直接编码 GADTs，并给出类型可靠性与关系模型。
只需几个平方根，量子计算就像 Pi 一样简单
给 rig groupoid 增加两个映射和三条等式，即可得到量子计算通用语义及可靠完备等式理论。
面向含局部变量程序的高效自底向上合成
提出 lifted interpretation，使自底向上合成能高效搜索含局部变量（如 lambda）的程序，并实现 Web 自动化工具 Arborist。
宽松 Arm-A 架构上计算机程序设计的公理化基础：AxSL 逻辑
提出 AxSL 分离逻辑，支持 Arm-A 宽松内存下的模块化验证，并在 Iris 中机械化证明其相对 Arm-A 公理模型的可靠性。
多项式时间与依赖类型
将依赖类型与线性类型系统结合，用定量类型论保证项的计算复杂度为多项式时间。
将直接操作融合进函数式程序
提出基于操作的框架与 delta 语言 DM，将开发者对输出的直接操作自动融合进函数式源代码，实现代码不敏感的直接操作。
在 F* 中保护经验证的 IO 程序免受未验证代码影响
提出并验证 SCIO⋆ 安全编译框架，通过高阶契约与引用监控，使已验证 IO 程序与不可信上下文链接后仍满足全局轨迹性质。
数组系统的正则抽象
提出索引谓词抽象，将数组系统过近似为字符串重写系统，从而自动验证安全性与活性。
名义递归器作为epi-递归器
将名义递归器抽象为epi-递归器，比较其表达力并建立层级，结果在Isabelle/HOL中验证。
EasyBC：一种用于分组密码抗差分密码分析安全性分析的密码学专用语言
提出密码学专用语言 EasyBC 与基于 MILP 的自动流程，用于评估分组密码抗差分密码分析能力。
结构参数多态的参数化子类型
提出参数化子类型，一个可判定且严格推广刚性子类型的结构子类型片段，并给出饱和式判定过程与实现。
用依赖类型内化不可区分性
提出依赖不可区分性演算 DCOI，把不可区分性内化为类型检查器相等性与观察者索引命题相等类型。
Quotient Haskell：面向所有人的轻量级商类型
提出证明义务可由 SMT 判定的商类型，并实现为 Liquid Haskell 扩展 Quotient Haskell。
文档的核心演算：或者，Lambda：终极文档
提出文档演算，将文档语言分层形式化，为混合文档与程序的语言提供形式基础并支持反应式等特性。
ReML 中的显式效应与效应约束
提出 ReML 语言，通过显式效应与效应约束支持区域基内存管理，并集成多态区域推断。
线性算术中的 Ramsey 量词
提出在线性整数/实数算术中消去 Ramsey 量词的多项式时间算法，并用于终止性等验证。
未装箱数据构造器：或者，cpp 如何判定停机问题
为 ML 系语言提出可选择性未装箱数据构造器，并给出拒绝表示混淆的静态分析与终止性判定算法。
基于类型的渐进类型（gradual typing）性能优化
提出判别式类型化：乐观推断函数类型并生成优化/未优化双版本，在保持安全性的同时大幅降低渐进类型开销。
带效应的软件契约
在效应处理器语境下提出通用效应契约系统，并证明契约不会不当干扰程序执行。
连续下推 VASS 中的可达性
证明连续下推向量加法系统（PVASS）的可达性是 NEXPTIME 完全的，且对二进制/一元编码与有界栈等条件具有鲁棒性。
Future、状态与交互中的解缠
将解缠从 fork/join 推广到 future 并行，并证明其在状态、交互下的保持及无死锁性。
DisLog：面向 disentanglement 的分离逻辑
提出首个静态验证并行程序 disentanglement 的并发分离逻辑 DisLog，并提炼 DisLog+，全部在 Coq/Iris 中机械化。
多态可达性类型：在高阶泛型程序中跟踪新鲜性、别名与分离
提出多态可达性类型系统，用新鲜性限定符与轻量/有界多态健全跟踪高阶泛型程序中的生命周期、别名与分离。
Quantum FPC 的富化预层模型
将超算子模型扩展到高阶量子程序，基于富化预层，并证明其是带递归类型的 Quantum FPC 的完全抽象模型。
有界高度无序树上的多项式正则函数
证明有界高度无序树上单射一阶解释的等价问题可判定，并给出精确刻画它的类型化演算。
202374 篇 · 7(POPL)
概率程序的平滑性分析及其在优化变分推断中的应用
提出概率程序平滑性静态分析，自动识别可微部分，改进路径梯度估计器且无需人工干预。
你只需线性化一次：切向量转置成梯度
将反向模式自动微分分解为正向模式、线性/非线性解压与线性部分转置，并证明其正确性。
用于贝叶斯编程的仿射单子与惰性结构
提出用于贝叶斯编程的仿射概率单子与惰性结构语义，给出适配惰性的推断方法及 Haskell 库 LazyPPL。
类型保持、依赖感知的 guide 生成：面向可靠且有效的摊销概率推断
用行为类型系统驱动类型导向翻译，自动生成概率程序的 guide，保证可靠性并提升摊销推断效果。
CFL 可达性问题的细粒度复杂度
在细粒度复杂度框架下确定 CFL 可达性的精确指数，并证明 Dyck-2 的 Ω(n^2.5) 下界。
不可判定问题的可见证性
提出“可见证性”概念，证明多数不可判定问题可计算地从任意可判定近似构造出反例输入。
CN：用分离逻辑精化类型验证系统 C 代码
设计并实现 CN——面向系统 C 代码的分离逻辑精化类型系统，并验证 pKVM 组件。
ADEV：概率程序期望值的健全自动微分
提出 ADEV，将前向自动微分扩展到概率程序，使变换后程序的期望值等于原程序期望的梯度。
当少即是多：弱算术理论中的后承发现
提出弱公理化乘法的非线性算术理论及后承发现算法，用于生成循环不变式并证明程序安全性质。
面向自动程序验证的 HFL(Z) 有效性检查
提出 HFL(Z) 公式有效性的自动判定方法，配合归约实现对高阶函数式程序各类时序性质的统一全自动验证。
基于整数线性规划的单源单目标交错 Dyck 可达性
提出用路径表达式与整数线性规划求解单源单目标 InterDyck 可达性，避免传统汇总边并显著加速。
为 GPU 计算的中间表示夺回控制权
为 SPIR-V 结构化控制流建立形式模型，据此修正规范、校验工具，并用模型引导的模糊测试发现 20 个编译器缺陷。
用于时序验证的模块化原始-对偶不动点逻辑求解
提出模块化原始-对偶方法求解带背景理论的一阶不动点逻辑 µCLP，并将其用于时序验证。
一种摊还期望运行时间演算
提出 aert 演算，以最弱前置条件风格定量推理随机算法在动态内存下的摊还期望运行时间。
Choice Trees：在 Coq 中表示非确定性、递归与不纯程序
提出 ctrees，一个在 Coq 中统一建模非确定性、递归与不纯程序并支持双模拟/精化推理的余归纳树单子。
DimSum：多语言语义与验证的去中心化方法
提出去中心化的多语言语义与验证框架，各语言可独立定义、通过事件与组合子组合，并在 Coq 中验证跨语言编译器。
关系验证的对齐代数
提出 BiKAT 代数统一关系验证中的对齐表示，支持等式推理并导出 forall-exists 性质的 RHL 规则。
Kater：自动化弱内存模型元理论与一致性检查
将弱内存模型元理论问题归约为正则语言包含，并自动生成一致性检查，集成到 GenMC。
面向可数非确定性与概率选择的步进索引逻辑关系
为含可数非确定性与概率选择的高阶语言构建步进索引逻辑关系，并给出可靠完备的上下文等价理论。
并发程序验证算法中的分层交换性
将交换性关系作为并发程序验证中的一等对象，提出抽象交换性框架与分层组合证明规则。
概率资源感知会话类型
提出概率会话类型与嵌套多重宇宙语义，实现自动期望资源分析并开发 NomosPro 工具。
论字符串约束的表达能力
系统比较20种字符串约束逻辑理论的语言表达能力，并研究跨理论可表达性的可判定性。
不可实现性逻辑
提出首个用于证明程序合成问题不可实现（无解）的 Hoare 风格证明系统，可对无限程序集的执行进行上近似。
Grisette：将符号编译作为函数式编程库
提出纯函数式、静态类型的符号求值库 Grisette，以有序守卫合并路径，显著缩小约束并加速求解。
通过众所周知的程序变换实现高效对偶数反向模式自动微分
提出用线性因子分解等常见函数式程序变换，将对偶数反向模式自动微分优化为复杂度正确且可在 Haskell 中高效实现的算法。
基于终止性证明的最优 CHC 求解
提出将最优 CHC 求解的最优性检查归约到终止性分析，并用约束合成终止论证来实现。
Dargent：验证数据布局精化的银弹
提出 Dargent 数据布局描述语言与精化框架，为 Cogent 生成带形式正确性证明的 C 代码，消除 marshalling 复制开销。
从 SMT 到 ASP：求解 Datalog 综合中“规则选择”问题的基于求解器的方法
提出三种基于求解器的方法求解 Datalog 规则选择综合问题，其中编码为 ASP 的方案比现有技术快约 9 倍且综合出更高质量的程序。
调和 Shannon 与 Scott：可计算信息格
提出可计算信息格 LoCI，融合 Shannon 定性信息论与 Scott 域论，统一刻画程序信息流及其可观察精度。
高阶 MSL Horn 约束
提出高阶 MSL Horn 约束类并给出基于消解的判定过程，证明其与 HORS 模型检测可相互归约，并应用于高阶程序验证。
面向垃圾回收下堆空间的高层分离逻辑
提出带空间信用与可堆叠断言的高层分离逻辑，在含GC的高层语言中模块化推理堆空间，并在Coq/Iris中机器化验证。
比较式合成：通过查询学习近最优网络设计
提出比较式合成框架，通过 Validate/Compare 查询在目标不明确时合成近优网络设计，并实现 Net10Q。
babble：使用 E-Graph 和反合一学习更好的抽象
提出 LLMT 库学习算法，利用 E-Graph 和等式饱和及 E-Graph 反合一，高效提取可复用库函数，压缩优于 SOTA。
Qunity：一个统一量子与经典计算的语言
提出统一量子与经典计算的语言 Qunity，以统一语法和指称语义保证量子有效性，并可编译到 OpenQASM。
CoqQ：量子程序的基础性验证
在 Coq 中构建深度嵌入的量子编程语言与程序逻辑，并机器化证明其相对于指称语义的可靠性。
面向库学习的自顶向下合成
提出语料引导的自顶向下合成算法 Stitch，从 DSL 程序语料中高效学习库抽象，速度与内存大幅优于 DreamCoder。
条件上下文精化
提出 CCR，首个将精化与分离逻辑统一、同时支持条件规约与传递组合的低层系统验证框架。
FlashFill++：通过 Cut 直击关键来扩展示例编程
提出 cut 函数与 guarded DSL，把示例编程合成扩展到含非 EI/EE 算子的大型 DSL，并实现 FlashFill++。
效应化 JIT 中的形式验证本机代码生成：将 CompCert 后端转变为形式验证的 JIT 编译器
在 Coq 中实现并验证带效应的 JIT，动态复用 CompCert 后端生成经证明的本机代码。
MSWasm：可靠地强制执行不安全代码的内存安全执行
为 Wasm 引入语言级内存安全抽象，形式化证明良类型程序内存安全，并实现支持多种强制机制的编译器。
从非递归表达式归纳合成结构递归的函数式程序
提出基于块剪枝的归纳合成方法，从输入输出示例合成结构递归的函数式程序，并在 Trio 系统中达到 98% 的基准求解率。
在 Serverless 上正确执行微服务应用
提出 mu2sls 框架，以事务和异步调用原语在 Serverless 上正确执行 Python 微服务并提供形式化保证。
带 answer-effect 修改的时序验证：支持定界续延的依赖时序类型与效应系统
提出支持 shift0/reset0 的依赖时序类型与效应系统，通过 answer-effect 修改实现事件序列的时序验证。
迈向高阶数学操作语义
提出高阶抽象GSOS理论，以dinatural变换刻画高阶语言操作语义，并给出通用组合性结果。
非直谓观测等价
扩展观测类型理论，引入证明无关的非直谓宇宙，证明 conversion 可判定且理论在 MLTT 中可归一化，兼容 UIP 与非直谓性。
松弛内存并发下库抽象的一种操作方法
针对 RC11 弱内存模型给出操作语义与通用库正确性条件，使客户端可用规范代码推理程序行为。
为野兽系上领结：F⋈ 中的重载、eta 展开与可扩展数据类型
提出 F⋈ 核心语言，用对偶不相交关系驯服 merge，使 union、intersection 和重载共存且类型安全、确定。
尾递归模上下文：一种等式方法
将 TRMc 推广为 TRMC，从规约等式推导通用算法，并在 Koka 实现支持非线性控制的混合版本。
定量重写基础
提出基于 quantale 的定量与度量重写理论，并将 Newman 引理、Church-Rosser 定理等核心结果推广到该框架。
消息传递通信模型的偏序视角
基于并发行为提出统一的消息传递通信模型层级，并证明其均可用一元二阶逻辑公理化。
基于 O(1) 采样的动态数据竞争检测
提出首个亚线性时间随机动态数据竞争检测器，仅处理常数个事件即可高概率发现远距离竞争且无误报。
Hefty 代数：高阶代数效应的模块化精化
提出 Hefty 代数，将高阶操作的展开过程模块化，从而在不改接口、不重编译的情况下支持高阶代数效应的实现与精化。
密码协议等式证明的核心演算
提出核心演算 IPDL，支持密码协议观察等价的等式证明并机器化到 Coq。
SSA 翻译是一种抽象解释
将 SSA 翻译重新表述为抽象解释式静态分析，使其可与其它分析单遍组合并用于 C/机器码分析器。
快速余代数互模拟最小化
提出一个通用余代数互模拟最小化算法，仅需可计算的函子作用，并在基准上优于专用工具。
局部无名集合
用范畴论与名义技术为局部无名语法表示建立等式公理与初始代数语义，并证明其范畴等价于有限支撑 M-集拓扑斯。
通往持久线性化（durable linearizability）之路
提出通用、模块化、增量的证明技术，用于建立持久并发数据结构的持久线性化。
高阶锁的无泄漏与无死锁
提出基于共享拓扑的高阶锁理论，证明良类型程序无死锁且无内存泄漏，并在 Coq 中机器化验证。
统一框架下不同 Lambda 演算的定量 Inhabitation
提出统一框架求解 λ! 的定量 inhabitation，并为可编码进 λ! 的多种 lambda 演算导出 inhabitation 算法。
制造类型差异：交集类型上的减法作为广义记录操作
提出基于子类型与不相交关系的通用类型差运算，将记录上的删除/更新操作推广到函数与交集类型。
结合函数式合成与自动机合成以发现因果反应式程序
提出在函数式合成与自动机合成间迭代的算法，从观测数据中合成因果反应式程序。
上下文限界的上下文无关规范验证
证明上下文限界下多栈下推系统对 Dyck 等上下文无关规范的精化验证可判定且 coNP 完全。
高阶逻辑中可容许的 Types-to-PERs 相对化
首次系统定义并证明 HOL 中 Types-to-PERs 相对化的可容许性，并实现 Isabelle 按需相对化工具。
一种用于多项式时间的通用非干涉策略
提出面向对象语言中捕获多项式时间函数的通用非干涉策略，并用形状分析给出可判定保守实例。
因果性的几何：多令牌交互几何及其因果展开
为高阶并发语言 IPA 建立多令牌 Petri 网机器，并用并发博弈证明其计算充分性。
静态可消解歧义
提出首个高效、实用且经 Coq 证明正确的静态可消解歧义方案，并集成到 OCaml 解析器。
Coq 中分治递归的基于类型的方法
提出一种用代数与类型纪律刻画分治递归的方法，并在 Coq 中实现验证，无需结构递归或依赖类型。
带动态提升的 Proto-Quipper
为 Proto-Quipper-M 增加动态提升，使量子测量结果可影响后续电路生成，并给出类型、操作与范畴语义及可靠性证明。
面向所有类型的递归子类型
提出 F≤μ，将 iso-recursive 类型与有界量化结合，证明子类型可判定、传递且保守，并在 Coq 中形式化。
串并联图的稳健理论
提出同步串并联图，证明其确定性/非确定性自动机等价于MSO与分级μ演算，并给出确定化与判定过程。
用带图（Tape Diagrams）解构关系演算
提出带图，为有限双积的 rig 范畴给出可靠且完备的图解语言，并用于关系演算。
线性一致性的组合式理论
用 Karoubi envelope 为线性一致性建立组合语义，给出不依赖原子性与 happens-before 的新表述并重建其理论。
在证明相关模型中，证明为何是相关的？
在范畴化图模型中，证明相关解释包含完整类型推导，可重构近似项，并将λ理论刻画为Böhm树相等。
宇宙多态性的序理论分析
用严格偏序范畴上的单子与位移代数刻画依赖类型论中的宇宙多态，并给出可实现的分层方案。
202265 篇 · 6(POPL)
一种多项式逼近：为多种表示与舍入模式生成初等函数的正确舍入结果
提出用 n+2 位 round-to-odd 多项式逼近，一次生成支持多种精度与全部 IEEE 舍入模式的正确舍入初等函数库。
用于 Clarke 雅可比矩阵静态分析的对偶数抽象
提出对偶数抽象域，可靠过近似 Clarke 雅可比，并实现 DeepJ 分析非光滑神经网络的 Lipschitz 鲁棒性与优化景观。
对“关于推理的推理”的推理：带嵌套查询与递归的概率程序的语义与上下文等价
首次为含嵌套查询与一般递归的概率程序给出互递归语义，并建立上下文等价的关系推理原则。
神经网络的区间通用逼近
提出区间通用逼近定理，并证明构造精确区间分析神经网络本质困难。
PRIMA：通过可扩展凸包近似实现通用且精确的神经网络认证
提出 PRIMA，用可扩展凸包近似实现通用且精确的神经网络形式认证。
CFA 归来：即使对面向对象程序，调用点敏感也能优于对象敏感
挑战对象敏感优于调用点敏感的传统观点，在上下文隧道机制下证明调用点敏感可模拟对象敏感且更精确可扩展。
可证明正确、渐近高效的高阶反向模式自动微分
提出高阶反向模式自动微分的简单高效实现，并证明其正确性与渐近复杂度。
通过高层调度重写实现经验证的张量程序优化
在 Coq 中构建轻量框架，用一系列经验证的语义保持重写，对纯函数式数组语言写的张量核进行调度优化。
并发不正确性分离逻辑
将不正确性分离逻辑扩展到并发程序，提供参数化框架检测竞态、死锁和内存安全错误并保证真阳性。
抽象解释中的部分（不）完备性：限制程序分析中的不精确性
提出抽象解释中误差传播理论与部分完备性概念，并用证明系统估计分析累积误差上界。
交错 bidirected Dyck 可达性的可判定性与复杂度
系统解决交错 bidirected Dyck 可达性的可判定性与复杂度，改进上界并确立可判定与不可判定边界。
一种用于负相关性的分离逻辑
提出概率分离逻辑 LINA，用两种分离合取分别刻画独立性与负相关性，并验证哈希数据结构等随机程序。
带合并的符号求值的形式化基础
首次为支持状态合并的可复用符号求值器建立形式语义，并在 Lean 中机械化证明其可靠性与完备性。
动态双向 Dyck 可达性的高效算法
提出首个双向图上动态 Dyck 可达性算法，每次边更新 O(n·α(n))、全对查询 O(1)。
性质导向可达性作为单调理论中的抽象解释
将命题PDR重构为单调理论中的抽象解释，并用最佳变换器刻画其不变式推断。
并行计算图的静态预测
提出图类型（graph types），静态推断并行程序所有可能的计算图，并用于死锁检测与开销分析。
真正无状态的最优动态偏序归约
提出 TruSt 算法，使并发程序动态偏序归约同时做到每等价类仅探索一个交错且内存消耗为线性。
借助带优先级与变量的转换器求解含 RegEx 相关函数的字符串约束
提出首个原生支持 RegEx（贪婪/懒惰、捕获组）的字符串理论与求解器，核心为带优先级的流式字符串转换器 PSST。
基于天使式执行的自底向上递归函数式程序合成
提出基于天使语义与版本空间学习的自底向上递归函数式程序合成方法。
模代数数据类型与递归函数求解约束 Horn 子句
提出 IC3 启发的 Racer 算法，在 ADT 与 catamorphism 下求解 CHC，自动合成归纳不变式并保证找到不安全反例。
一个成本感知的逻辑框架
提出 calf 成本感知逻辑框架，以依赖类型论统一程序行为与成本推理，并在 Agda 中机器化验证算法复杂度。
CFL 可达性的次三次证书
证明 CFL 可达性存在 O(n^2) 大小的存在性与非存在性证书，并可在次三次时间内验证。
连接图：一种基于分离逻辑证明无死锁的方法
提出连接图抽象，用分离逻辑证明无死锁与无内存泄漏，并在 Coq 中机械化，首次为高阶二元会话类型语言提供机械化证明。
再探 Profile 推断
提出有理论保证的高效 Profile 推断算法，修正采样 Profile 并提升 PGO 生成代码性能。
依赖类型的数据平面编程
提出基于可判定精化的依赖类型 P4 方言 Π4，为数据平面程序提供轻量级静态验证。
归纳对偶：不变式的原始-对偶搜索
提出状态与谓词间的归纳对偶性，并据此构造首个真正原始-对偶的不变式推断算法，可验证分布式协议。
论类型分支、联合消除与出现类型（occurrence typing）
扩展联合/交集类型系统加入 type-case，证明其与联合消除可涵盖 occurrence typing，并给出类型重建算法。
无税隔离：WebAssembly 与 SFI 的近零成本转换
提出零成本转换条件，改造 Lucet Wasm 运行时并构建静态验证器 VeriZero，在保证 SFI 安全的同时消除上下文切换开销。
关系式 e-matching
提出基于关系连接与查询计划的 e-matching，保证最坏情况最优运行时间，并在 egg 中大幅加速。
软件模型检测作为循环证明搜索
将多种软件模型检测算法统一为循环证明系统中的证明搜索策略，并揭示极大保守性启发式的意义。
论不正确性逻辑与带顶元素和测试的 Kleene 代数
证明 KAT 无法直接表达不正确性逻辑，并提出 TopKAT 通过顶元素刻画陪域，表达不正确性三元组并证明其规则可靠。
使用名义内存模型的可验证 C 程序编译
提出基于名义技术的内存模型，突破 CompCert 块式内存模型限制，支持开放/并发程序的可验证编译。
基于 Galois 依赖的联动可视化
提出基于 Galois 连接的双向程序切片动态分析，支持可否定选择，为 brushing and linking 提供语言基础。
有限变量逻辑中的公式学习
提出通用自动机理论技术，在有限变量逻辑中实现语法受限的公式与项精确学习、可实现性判定和合成。
通过范畴论逻辑关系构造有效应 λ-演算的完全抽象模型
提出范畴论逻辑关系构造，为带和类型、效应操作与基元的计算 λ-演算生成可靠且完全抽象的模型。
Simuliris：一个用于验证并发程序优化的分离逻辑框架
提出 Simuliris，首个在公平调度下证明利用未定义行为的并发程序变换保持终止的模拟技术。
Pirouette：高阶类型化函数式编排编程
提出 Pirouette，一种带类型的高阶函数式编排编程语言，可将中心化程序投影为分布式节点程序，并保证消息类型健全与无死锁。
Twist：量子程序中纯性与纠缠的可靠推理
提出首个具备纯性类型系统的量子语言 Twist，可靠推理纠缠，结合静态分析与运行时验证。
SolType：面向 Solidity 算术溢出的精化类型
提出 Solidity 精化类型系统 SolType，可自动推断标注并证明算术运算无溢出/下溢。
扩展 Intel-x86 一致性与持久性：形式化 Intel-x86 内存类型与非临时存储的语义
将 Intel-x86 一致性/持久性语义扩展到非临时写、不可缓存、写合并和写穿内存类型，并证明操作式与声明式模型等价。
效应与 coeffect 的关系理论
提出 corelator（余单子松弛扩张）与程序关系演算，为含效应与 coeffect 的高阶语言建立程序细化/等价的关系理论。
分号泄漏：面向松弛内存并发的组合式语义依赖
通过前置条件和谓词变换器族，为松弛内存并发中的顺序组合提供组合式语义。
二阶抽象语法的形式化元理论
在 Agda 中基于初始代数语义自动生成带变量绑定与二阶替换的语言元理论框架。
线性循环中什么是可判定的？
论文刻画了带半代数谓词的简单线性循环在MSO模型检测下的可判定片段，并指出放宽条件需数论突破。
分离合取的量子解释：基于分离逻辑的量子程序局部推理
提出量子分离合取的量子解释，并构建支持局部推理的 Hoare 风格量子程序验证框架。
变分量子编程的语义
为混合经典-量子变分编程语言建立可靠且计算充分的指称语义，连接概率与量子模型。
VIP：验证带有整数-指针转换的真实世界 C 惯用法
提出 VIP 内存模型，用显式 provenance 构造简化整数-指针转换，并实现可验证真实 C 代码的 RefinedC-VIP。
面向垃圾回收下堆空间的分离逻辑
提出 SL♢，用空间信用与 pointed-by 断言在含分配、GC 与并发的语言中控制堆空间消耗并证明其可靠性。
使用 match types 的类型级编程
提出 match types——类型级的模式匹配，在基于 System F<: 的演算中形式化并证明可靠性，并在 Scala 3 编译器中实现。
分层与基于对象的博弈语义
提出基于对象的分层博弈语义，用对象策略与正则映射刻画可认证抽象层及其并发扩展。
二元会话的公平终止
提出首个保证二元会话公平终止的类型系统，并首次实际采用公平子类型。
带效应的程序距离化
将差分逻辑关系推广到带效应高阶程序，用 quantale 度量值与计算效应之间的距离。
不经意代数数据类型
提出不经意代数数据类型及带安全类型系统的语言，支持对树等递归私有数据进行安全计算。
Girard 直觉主义证明网（proof-nets）的细粒度计算解释
提出项演算 pn，以细粒度方式刻画直觉主义线性逻辑证明网的静态结构与动态归约，并证明合流、强规范化等性质。
安全、模块化的包处理流水线编程
提出 Lucid 2.0 语言与类型系统，保证交换机程序一致顺序访问数据，并支持模块化包处理流水线编程。
对数与程序测试
提出无需嵌入-投影对的机械化单态化，将多态函数用于自动属性测试，并揭示合适类型计算为对数。
从增强余归纳迈向增强归纳
为归纳行为关系建立类似余归纳增强的证明理论，并以权重保持条件保证增强函数的可靠性。
线程池的上下文限界验证
证明线程池上下文限界布尔程序安全性验证为 EXPSPACE 完全，并给出基于向下闭包的紧致编码。
从协程到状态机的可认证推导
提出在 Coq 中以策略形式实现的编译器，将高阶协程自动可验证地编译为显式状态机。
量子信息效应
提出隐藏与分配两种对偶量子信息效应，建立可表达不可逆量子计算（含测量）的类型与效应系统，并给出范畴语义。
并发快照算法的可见性关系推理
用可见性关系为 Jayanti 的三个并发快照算法构建模块化、可复用的线性化证明。
Mœbius：使用上下文类型的元编程——System F 能对自身进行模式匹配的阶段
提出 Mœbius 元编程语言基础，支持多态代码生成与对开放代码的模式匹配，并证明类型保持。
观察性相等：这次一劳永逸
提出 TTobs，为依赖类型论中每个类型配备满足函数外延、命题外延和 UIP 的同一关系，并证明规范化、正则性与可判定性。
带类型类的分阶段编程：类型化 Template Haskell 的一个规范
提出 staged type class constraints，形式化为源演算 λ⇒ 与核心演算 F，证明类型健全性，解决代码引用与类型类的不健全交互。
可逆编程中的对称性：从对称 rig groupoid 到可逆编程语言
为可逆布尔电路语言 Pi 建立基于弱 groupoid 的指称语义，并证明其与有限类型 univalent 子宇宙的 groupoid 等价及 Curry–Howard–Lambek 对应。
202161 篇 · 5(POPL)
论双向交错 Dyck 可达性的复杂度
证明了双向交错 Dyck 可达性的首个可判定变体 D1⊙D1 属于 PTIME，并证明 k≥2 时为 NP-hard，且其过近似更精确。
一种为新型浮点变体生成正确舍入数学库的方法
提出用线性规划生成多项式逼近正确舍入值，为新型浮点格式自动构建正确舍入数学库。
PCF 中的自动微分
证明 PCF（含实数的高阶图灵完备语言）中前向与反向自动微分在温和假设下几乎处处正确。
概率程序的相对完备验证：一种用于基于期望推理的表达性语言
提出一种表达力充分的定量断言语法，使概率程序基于期望的验证系统达到相对完备。
概率敏感性的前期望演算
提出关系前期望演算，用Kantorovich距离上界约束概率程序两次执行输出的分布距离。
PerSeVerE：ext4 下用于验证的持久性语义
形式化 ext4 与 C/C++ 弱内存的持久性语义，提出模型检测验证方法并发现编辑器缺陷。
CUDA 内核求值代价的建模与分析
提出面向 CUDA 内核的定量程序逻辑与代价语义，可自动推导符号化资源上界并检测性能瓶颈。
判定差分隐私方案的准确性
提出基于程序不连续性的通用准确性定义，并研究差分隐私方案准确性判定的可判定性与判定过程。
简化多面体模型中的依赖归约
将多面体模型中的依赖归约优化形式化为整数双线性规划，并提出保持依赖的启发式算法。
学习归纳不变式的边界
将精确概念学习理论引入不变式推断，提出 fence 条件，首次给出插值式不变式推断的多项式复杂度结果。
名字生成的概率编程语义
将准Borel空间语义用于ν演算，证明其可靠且在一阶类型上完全抽象，建立随机采样与新鲜名字生成的类比。
一种实用的递归定义模式系统
提出一种实用的模式系统，静态检测 call-by-value 递归定义中的恶性循环，并成功替换 OCaml 的不健全语法检查。
egg：快速且可扩展的等式饱和
提出 rebuilding 与 e-class analyses 两项技术，使 e-graph 在等式饱和场景下兼具高性能与可扩展性，并实现开源库 egg。
Blade：自动消除密码代码中的推测性泄漏
提出 Blade，用类型系统与 protect 原语自动切断推测性秘密的数据流，消除密码代码中的推测泄漏。
JIT 编译器中形式化验证的推测与去优化
提出显式化去优化同步点与推测假设的 JIT 中间表示，并在证明助手中验证若干推测优化。
异步超属性的自动机与不动点
首次提出异步超属性的自动机模型与不动点演算 Hµ，并给出可判定近似分析。
同步保持型竞态的最优预测
提出同步保持型竞态，并给出可靠完备、时空近最优的预测算法，证明其恰为竞态预测可处理边界。
结合自顶向下传播与自底向上枚举的归纳程序合成
提出 Duet，将自顶向下传播与自底向上枚举结合，实现可扩展且通用的归纳程序合成。
语义引导的程序合成
提出 SemGuS 框架，允许以递归大步步语义定义合成问题，并用 CHC 证明搜索同时合成程序与证明不可实现性。
面向效应处理器（effect handlers）的分离逻辑
提出内建支持浅层与深层效应处理器的分离逻辑，实现局部推理并基于 Iris 完成模块化验证。
驯服重写：一种带计算假设的类型论
提出重写类型论 RTT，允许把计算假设写成重写规则并自动用于类型检查，同时保持类型可靠性。
Andersen 指针分析的细粒度与并行复杂度
刻画 Andersen 指针分析（APA）的细粒度与并行复杂度，证明一般情形 Θ(n³) 最优，受限情形近矩阵乘法并可并行。
交集类型与（正）几乎必然终止
用非幂等交集类型同时刻画随机λ演算的收敛概率与正几乎必然终止，并证明其可靠完备且递归论最优。
数据流精化类型推断
提出参数化精化类型系统，用抽象解释刻画数据流语义并导出推断算法，统一并推广现有方法。
在线性递推序列上判定 ω-正则性质
证明简单线性递推序列的符号描述几乎周期，并给出判定前缀无关 ω-正则性质的过程。
验证上下文无关 API 协议的正确使用
提出用 CFG 过近似程序 API 调用序列并做语言包含检查与精化，验证上下文无关 API 协议使用。
λS：具有高阶函数与数据类型的可微编程的可计算语义
提出可微编程语言 λS，首次为高阶函数、高阶导数与 Lipschitz 不可微函数提供可计算语义。
可归约控制流图上 SPMD 发散性的抽象解释
提出首个适用于可归约 CFG 的 SPMD 均匀性抽象解释，精度与 LLVM 默认分析相当且带 Coq 机械化正确性证明。
论并发分离逻辑的代数抽象
论文用PCM间保持结构的部分函数与分离关系，对并发分离逻辑中的所有权转移进行了代数形式化。
概率编程的悖论：以及如何用无穷小概率对零测度事件进行条件化
指出朴素似然累积在条件化零测度事件时导致悖论，并提出用无穷小概率累积执行概率程序来消除悖论。
内涵数据类型精化：应用于模式匹配安全性的可扩展验证
提出用于模式匹配安全验证的内涵数据类型精化类型系统，其推断可靠、完备且接近线性时间。
一个经过验证的量子电路优化器
提出首个用 Coq 完全验证的量子电路优化器 VOQC，基于深嵌入 SQIR 并证明优化正确性。
一个带使用感知语义的分级依赖类型系统
提出 GraD 分级依赖类型系统，并给出基于堆的使用感知语义与资源核算可靠性证明。
使用未初始化能力实现高效且可证明的局部能力撤销
提出未初始化能力及其机器化验证程序逻辑，在不暴露内存初值的前提下实现高效局部能力撤销并证明能力安全。
高阶（摊销）代价分析的统一类型论
提出 λ-amor 类型论，用模态势类型统一高阶函数式程序的摊销代价分析，并能嵌入已有代价类型系统。
异步多参与方会话的精确子类型
首次形式化异步多方会话的精确子类型，并证明其可靠且完备，实现安全进程替换与异步消息优化。
驯服 x86-TSO 持久性
为 x86-TSO 非易失内存建立等价持久性模型，并给出到 x86 的健全映射与数据竞争自由保证。
Petr4：P4 数据平面的形式化基础
提出 Petr4，用定义式解释器与核心演算为 P4 数据平面建立形式化语义，并通过大规模测试和类型保持终止性证明验证。
针对 C11 风格内存模型验证观测鲁棒性
提出观测鲁棒性，将 C11 风格内存模型下的并发程序鲁棒性验证归约为顺序一致性下的可达性问题。
Dijkstra 单子永生：面向交互树的终止敏感规约
把 Dijkstra 单子框架扩展到交互树，为带代数效应的非终止交互式程序提供终止敏感的规约与验证。
分布式因果内存：高阶分布式分离逻辑中的模块化规约与验证
首次对因果一致分布式数据库实现进行模块化规约与验证，并在 Coq 中机器化证明。
Corpse Reviver：通过契约验证实现健全且高效的渐进类型
用软契约验证静态分析无类型代码，在编译期消除渐进类型边界的绝大多数动态检查，从而消除性能开销。
从静态语言到渐进语言的完全抽象
提出以“静态到渐进嵌入完全抽象”作为渐进语言设计准则，并机器化验证 GTLC^μ 满足该性质。
终止不敏感非干扰的机械化逻辑关系
提出支持递归类型、存在类型、标签多态与不可谓词多态的信息流控制类型系统，用逻辑关系与模态最弱前置条件证明终止不敏感非干扰。
渐进类型抽象的向前推进：精确且空间高效
将 AGT 的动态检查重构为对子类型关系的抽象解释，并借助前向完备性同时实现空间高效执行与可靠的运行时类型强制。
循环证明、系统 T 与收缩的力量
研究循环证明系统 C 的表达力，证明其与 Gödel 系统 T 等价，无收缩时恰好捕获原始递归函数。
持久 x86-TSO 下的可达性判定
证明持久 x86-TSO（Px86）模型下程序可达性问题是可判定的，并给出等价的良结构系统模型。
多面体模型的已验证代码生成
在 Coq 中形式化多面体模型到顺序代码的生成器，并证明其语义保持。
紧致闭范畴的计算解释：带负类型与分数类型的可逆编程
为可逆语言引入负类型和分数类型，定义操作语义并证明其构成紧致闭范畴，并实现可逆 SAT 求解。
偏理论的函子语义
提出偏理论的 Lawvere 式句法定义，用弦图项给出等式推理，并证明其模型范畴恰为局部有限可表范畴。
多线程共享内存程序活性性质的上下文限定验证
证明上下文限定下多线程共享内存程序（线程可动态生成）的公平终止等活性性质可判定。
超限步进索引用于终止性证明
提出超限步进索引的逻辑关系，首次证明含高阶共享可变状态的良类型程序终止。
使用无名标签的内在类型化编译
提出无名共上下文的全局标签表示，借助线性类型在 Agda 中实现按构造类型正确的编译器。
通过安全效应为程序计数器标签赋予语义
提出基于单子效应语义的框架，为信息流控制中程序计数器标签建立语义基础与新非干涉证明技术。
从证明生成集合变换
本文从逻辑证明中多项式时间合成嵌套集合变换，并证明经典功能性证明也足以生成 NRC 表达式。
用 univalence 内化表示独立性
提出用高阶归纳类型与 univalence 在依赖类型论中内化关系式表示独立性，并在 Cubical Agda 形式化验证。
论递归类型的语义表达力
证明 iso-递归与 equi-递归类型的 STLC 在语义表达力上等价，且均与项级递归的 STLC 等价。
钻石并非永恒：守卫递归反应式编程中的活性
提出 Lively RaTT，将 LTL 的时间步模态作为守卫递归的子模态，在保留守卫不动点的同时支持活性类型。
交互的（非）效率
在统一框架中比较四种抽象机，并用非幂等交类型证明交互抽象机的时间低效源于高阶类型。
可证明空间高效的并行函数式编程
提出可证明空间高效的并行函数式程序自动内存管理，将线程调度与GC结合，实现O(R*·P)空间与良好伸缩。
异步效应
提出异步代数效应核心演算 λæ，将操作调用解耦为信号与结果中断，并给出类型安全证明与原型。
2019145 篇 · 4(POPL)
通过原子条件检测浮点误差
提出基于原子条件数的动态分析，高效搜索触发大浮点误差的程序输入。
数值库中高浮点误差的高效自动修复
利用数值程序的数学特性检测并修复高浮点误差，工具 AutoRNP 在 GSL 的 20 个程序中修复了 19 个。
迈向概率程序的已验证随机变分推断
形式化随机变分推断中 REINFORCE 的隐含假设，并实现 Pyro 静态分析验证 model-guide 支撑匹配。
用于神经网络认证的抽象域
提出结合浮点多面体与区间的抽象域 DeepPoly，实现对深度神经网络可扩展且精确的认证。
不正确性逻辑
提出与 Hoare 正确性逻辑对偶的“不正确性逻辑”，用于形式化程序错误与缺陷推理。
分布式网络控制平面的抽象解释
用抽象解释降低分布式网络控制平面模拟的渐近复杂度，实现高效可达性分析。
定量分离逻辑：一种推理概率指针程序的逻辑
提出定量分离逻辑 QSL，为概率指针程序提供带局部推理的定量最弱前置条件演算。
高阶概率程序的形式验证：关于近似、收敛、贝叶斯推断与优化的推理
提出 PPV 逻辑族，用于验证带连续分布和高阶函数概率程序的近似、收敛、贝叶斯推断与优化性质。
面向自动数据建模的概率程序的贝叶斯合成
提出概率程序的贝叶斯合成框架，从观测数据自动构造数据建模 DSL 程序并保证其可靠性。
使用同步下推系统的上下文、流与字段敏感数据流分析
提出同步下推系统（SPDS），将过程调用/返回与字段读写编码为两个同步的 CFL 可达性问题，实现高精度且可扩展的上下文、流、字段敏感数据流分析。
低目标更难：概率程序验证中用于下界的归纳法
提出无需序列极限、仅需有限次应用循环体语义的概率程序期望值与运行时间下界归纳验证规则。
带条件化的高阶概率程序语义
用有序 Banach 空间上的线性算子为带条件的高阶概率程序建立指称语义，并验证 Gibbs 采样。
骨架语义及其解释
提出骨架语义，用统一解释从语言构造的语义骨架系统导出具体/抽象语义及一致性结果。
证明具有随机化、依赖于变量的终止时间的概率程序的期望敏感性
提出基于鞅的可靠方法，证明迭代次数随机依赖输入的概率 while 循环的期望敏感性，并可自动化与组合。
在 SlicStan 中基于密度的概率编程：高效、灵活且确定性
为 Stan 给出基于密度的操作语义，并设计可组合、自优化的 SlicStan，再保义翻译回 Stan。
确定性并行不动点计算
提出弱偏序 WPO 与确定性并行不动点算法，并通过 Pikos 在抽象解释中获得显著加速。
一个简单的可微分编程语言
为带反向模式微分的可微分编程语言建立操作语义与指称语义，并证明二者一致。
快速、可靠且有效完备的动态数据竞争预测
提出多项式时间且无假阳性的动态数据竞争预测算法 M²，对两进程完备并可动态判定完备性。
概率分离逻辑
提出概率分离逻辑 PSL，用分离建模概率独立，并验证密码构造的信息论安全性。
概率语言中可靠可编程推断的迹类型与指称语义
提出迹类型系统与指称语义，使可编程推断程序在构造上保证可靠性，覆盖变分、SMC、MCMC 等。
抽象外延性：论不完全抽象解释的性质
将程序外延等价推广到抽象解释诱导的抽象等价，证明任何非平凡抽象解释都会揭示程序的内涵差异。
JaVerT 2.0：面向 JavaScript 的组合式符号执行
提出统一的组合式符号执行方法，构建 JaVerT 2.0，首次为 JavaScript 支持基于双向溯因的自动组合测试。
A²I：抽象解释的抽象解释（元抽象解释）
提出并形式化离线与在线元抽象解释，用抽象解释分析程序分析器，并据此设计更高效精确的静态分析算法。
带线性否定的简单类型 λ-演算中的反向传播
将反向传播从一阶计算图扩展到带线性否定的简单类型 λ-演算，并保持一阶反向传播的效率。
连续格上的不动点博弈
提出连续格上的不动点奇偶博弈，统一刻画最小/最大解并推广 progress measure 至格化 µ 演算验证。
一种用于概率性不经意计算的语言
提出核心语言 Lambda Obliv，用子结构类型系统与「概率区域」静态保证概率程序的不经意性，并修复 ObliVM 的不健全性。
ARMv8-A、RISC-V 和 CHERI-MIPS 的 ISA 语义
使用 Sail 语言为 ARMv8-A、RISC-V、MIPS 和 CHERI-MIPS 架构建立严谨的可执行语义模型，支持模拟器与证明助手代码生成。
交互树：在 Coq 中表示递归与不纯程序
提出交互树，在 Coq 中表示递归、有副作用且可能非终止的程序，支持组合解释与弱互模拟等式推理。
保持常数时间的 C 编译器的形式化验证
通过改造 CompCert 并增强中间语言语义，机器化证明其编译保持密码学常数时间，从而消除计时侧信道。
Stacked Borrows：一种面向 Rust 的别名模型
提出 Stacked Borrows 操作语义，为 Rust 定义别名纪律，并用 Coq 证明其足以支撑内存访问重排优化。
量子关系霍尔逻辑（qRHL）
提出量子关系霍尔逻辑 qRHL，用于推理成对交互式量子程序并支持量子密码安全证明。
异常异步会话类型：无需层级（tiers）的会话类型
首次将异步会话类型与异常处理集成到函数式语言，给出核心演算与 Links 实现。
一种基于抽象栈的经过验证的组合式编译到机器码的方法
为 CompCert 内存模型引入抽象栈与细粒度栈权限，实现完整验证编译链并支持上下文组合编译。
溯源引导的 Datalog 程序合成
利用查询溯源信息引导 CEGIS，从输入输出规约高效合成 Datalog 程序。
面向统计概率编程的域理论
提出 quasi-Borel predomains，为含递归高阶类型与连续概率的统计概率编程语言建立充分指称语义，并证明交换性等价。
下一个 700 种关系程序逻辑
提出首个可为任意单子效应定义关系程序逻辑的通用框架，并给出语义基础与可靠逻辑核心。
使用句法分离的信号时序逻辑性质的有界模型检测
提出基于句法分离的 STL 有界模型检测算法，将验证归约为 SMT 可满足性，实现有界反驳完备。
可监控性探究：从分支时间到线性时间再返回
建立了带递归 Hennessy-Milner 逻辑的运行时可监控性理论，给出线性时间下可监控片段的表达力层级与监控保证。
一种经验证、高效的可验证汇编语言嵌入
在 F* 中嵌入 x64 汇编子集，借助依赖类型检查器运行经验证的 VC 生成器，实现汇编与 C 互操作的高效验证。
Liquidate your assets：在 Liquid Haskell 中推理资源使用
展示如何用 Liquid Haskell 的 refinement types 在同一框架中验证程序效率与资源使用。
弱内存一致性下的库正确性：声明式一致性模型中并发库的规约与验证
提出声明式框架，在弱内存一致性下对并发库进行组合式规约与验证。
并发随机化程序的分离逻辑
提出支持概率推理的并发分离逻辑 Polaris，并机器化验证随机化并发计数器与跳表。
数值循环的闭式形式
刻画线性数值循环何时可用有理数上的多项式和指数表示闭式形式，并给出可判定的安全性与终止性验证过程。
量子程序的定量鲁棒性分析
为含噪量子 while 程序建立语义与逻辑，定义并证明 ε-鲁棒性，支持纠错方案分析。
量子程序的关系证明
提出基于量子耦合的关系程序逻辑，用于验证量子程序的关系性质。
静态竞态检测器的真阳性定理
为 RacerD 静态竞态检测器证明真阳性定理，并给出与原版对比的实现评估。
底层沙箱化的高层收益
证明沙箱化可使受信任代码在任意不可信代码存在时仍保持类型安全（鲁棒安全），并在Coq中机械化验证。
带重置的数据流同步语言的机器化语义与经过验证的编译
在 Coq 中为带 reset 原语的数据流同步语言扩展机器化语义，并证明其编译器各趟的正确性。
静态分析中路径表达式的精化
提出路径表达式精化算法，保证不降低静态分析精度，并显著提升循环断言证明能力。
POSIX shell 的可执行形式语义
为 POSIX shell 定义可执行、机器化的小步操作语义 Smoosh，并通过测试验证其最符合 POSIX 标准。
通过可见性松弛的弱一致性规范
提出可见性松弛注释语言，为多一致性级别操作提供弱一致性规范并支持有效验证。
通过 Call-by-Push-Value 为函数式程序提取递推式
以 Call-by-Push-Value 为中间语言，从高阶递归函数式程序自动提取运行时间递推式，并给出指称代价语义。
概率模追踪抽象
提出用失败自动机上近似程序 trace、并将概率推理归约为逻辑推理的概率程序精度验证方法。
Iron：管理高阶并发分离逻辑中的义务
提出 Iron，一种高阶并发分离逻辑，可精确推理动态线程间可转移资源及其义务，并在 Iris 模型与 Coq 中证明其可靠性。
虚拟时间线：一种验证具有时间隔离的抢占式调度器的形式化抽象
提出虚拟时间线抽象，并在 Coq 中验证抢占式调度器实现，使实时内核获得时间与空间隔离。
未解释程序的可判定验证
提出 coherent 程序类，使未解释程序的完全自动验证可判定，并可在 Pspace 内完成。
面向高阶函数式语言的半朴素求值
将 Datalog 的半朴素求值扩展到 Datafun 的高阶函数式语言，支持一等关系与高阶函数递归。
类型引导的最坏情况输入生成
提出基于 AARA 类型推导的最坏情况输入生成方法，可证明资源界紧致并生成大规模测试输入。
合成替换类
提出借助自动合成的类间状态等价谓词，将候选类 R 合成为与原类 O 功能等价的替换类的技术。
TSO 下的参数化验证是 PSPACE 完全的
证明 TSO 下参数化并发程序可达性问题是 PSPACE 完全，并刻画初始读与原子 RMW 对复杂度的影响。
Concerto：一种具体解释与抽象解释相结合的框架
提出Concerto，通过具体解释分析框架实现、抽象解释分析应用代码，提升框架程序静态分析精度。
将无锁数据结构与内存回收解耦以进行静态分析
提出将无锁数据结构验证与内存回收解耦的静态分析方法，实现 Michael&Scott 和 DGLM 队列的全自动线性一致性验证。
不变式推断中的复杂性与信息
在 Hoare 查询模型下证明归纳不变式推断需指数查询，并证明 PDR 式丰富查询可较 ICE 学习指数加速。
判定单遍堆操作程序的内存安全
将可判定无解释程序扩展到别名感知映射更新，并在森林与单遍条件下判定堆程序内存安全。
D<: 的不可判定性及其可判定片段
证明 D<: 的类型检查与子类型不可判定，并给出两个可判定片段与判定算法。
基于关系扰动属性的增强示例合成
提出用关系扰动属性对示例合成施加语义偏置，自动增广示例以提升泛化能力。
利用静态相关性分析推断 frame conditions
提出相关性抽象域，自动推断程序输入输出间的相等关系，并用于生成 frame conditions、简化微内核不变式证明。
离散概率分布的最优近似采样
提出离散分布近似采样的理论框架，并构造在 k 位精度下统计与熵消耗均最优的采样算法。
code2vec：学习代码的分布式表示
提出 code2vec，将代码片段表示为定长向量，并通过预测方法名验证其语义表示能力。
少即是多：多方会话类型再探
提出更简单且更通用的多方会话类型理论，去除全局类型与二元对偶，修复类型安全证明缺陷，并支持可判定类型检查与活性保证。
复杂操作字符串操作程序的路径可行性判定过程
提出保证字符串操作程序路径可行性可判定的语义条件，并实现可扩展求解器 OSTRICH。
带类型洞的实时函数式编程
提出带类型洞的不完整函数式程序动态语义，求值可绕过洞并支持填洞后恢复，已在Agda机器化并实现于Hazel。
RustBelt 遇上宽松内存
通过同步幽灵状态，将 RustBelt 的 Rust 语义健全性证明扩展到宽松内存，并发现 Arc 库中的数据竞争。
Coq Coq correct! 在 Coq 中验证 Coq 的类型检查与擦除
在 Coq 中形式化验证 Coq 内核的类型检查器与类型/证明擦除，将可信代码基缩小为可信理论基。
未来属于我们：分离逻辑中的预言变量
首次在 Hoare 风格程序逻辑中引入 prophecy variables，并在 Iris/Coq 中形式化，用于验证并发算法的逻辑原子性。
CT-Wasm：面向 Web 生态的类型驱动安全密码学
在 WebAssembly 上引入类型驱动的严格扩展 CT-Wasm，用类型系统保证密码代码的信息流安全与恒定时间执行。
Intel-x86 架构的持久性语义
首次形式化 Intel-x86 的持久性语义 Px86，给出操作式与声明式定义并证明二者等价。
用事件结构为 thin-air reads 奠定基础
提出基于事件结构的并发内存语义，禁止 thin-air reads，并证明其与 promising 语义等价且更易扩展。
弥合编程语言与硬件弱内存模型之间的鸿沟
提出中间弱内存模型 IMM，将并发语言到 POWER/ARM 的编译正确性证明模块化，并在 Coq 中机器验证。
在 Go 中使用角色参数化会话类型进行分布式编程：面向动态实例化通信结构的静态类型端点 API
提出角色参数化多体会话类型理论，并为 Go 生成静态类型端点 API，以安全实现动态参与者协议。
探索 C 语义与指针来源（pointer provenance）
提出两种 C 指针来源语义方案，将其实现为可执行测试预言，并结合 CHERI 移植与 SPEC 插桩评估。
CompCertM：支持 C 与汇编链接及轻量级模块化验证的 CompCert
提出轻量级验证技术 RUSC，使 CompCert 在无限制条件下支持 C 与手写汇编的多语言链接，且验证开销低。
结构化堆操纵程序的合成
提出合成分离逻辑 SSL，将堆蕴含泛化为变换蕴含，通过证明搜索从分离逻辑规约合成指针程序。
通过隧道实现抽象安全的效应处理器
提出隧道语义，使高阶效应多态代码不会意外处理传入函数引发的效应，从而保证效应处理器既类型安全又抽象安全。
渐进类型：一个新的视角
提出更语义化的渐进类型解释，并用 subtyping 与 materialization 统一渐进化三种多态类型系统。
类型引导的抽象精化程序合成
提出 TYGAR，以抽象类型图可达性搜索结合不可类型性证明迭代精化，实现多态组件的高效类型导向程序合成。
Actris：分离逻辑中基于会话类型的推理
提出 Actris，将基于会话类型的一等协议机制融入并发分离逻辑，用 Coq 机器化验证消息传递程序的功能正确性。
StkTokens：使用线性 capability 强制良括号控制流与栈封装
提出并形式化 StkTokens 调用约定，借助硬件不可复制的线性 capability，证明其在 capability 机器上保证良括号控制流与局部状态封装。
Hamsaz：复制协调分析与合成
自动分析顺序对象的冲突与依赖关系，并为分布式复制合成避免不必要协调且满足完整性与收敛的对象。
火三角：如何混合替换、依赖消去与效应
提出类型论中替换、依赖消去与效应不相容的 no-go 定理，并给出依赖 CBPV 演算 ∂CBPV 以调和三者。
FrAngel：带控制结构的基于组件的程序合成
FrAngel 通过挖掘部分成功程序中的代码片段并用 angelic 条件占位控制结构条件，实现带循环等控制结构的组件式合成。
基于示例的可视化
提出组合式示例驱动可视化合成，将任务分解为两个 DSL 合成问题，并用双向程序分析处理不精确中间规约。
渐进性与参数性：再次携手
通过显式化类型名生成，提出同时满足渐进性与参数性定理的 System F 渐进扩展。
Guarded Kleene Algebra with Tests：未解释程序的近乎线性时间验证
提出 GKAT，利用其（余）代数理论，使未解释命令式程序的等式推理达到近乎线性时间。
cubical 计算类型论中的高阶归纳类型
扩展笛卡尔 cubical 计算类型论，引入索引 cubical 归纳类型模式并证明其可规范性定理。
LRU 缓存的快速精确分析
提出基于抽象解释的 LRU 缓存精确分析，兼顾高效与精确，并证明该分析问题一般 NP 完全。
LWeb：多层 Web 应用的信息流安全
提出 LWeb，将 LIO 信息流控制与 Yesod 结合，在数据库 Web 应用中执行标签策略并机器化证明无干扰。
面向量子编程的博弈语义
首次为完整量子λ演算给出组合式、交互式博弈语义模型，并证明其计算充分性。
渐进类型理论
提出渐进类型理论 GTT，公理化渐进转换演算的程序等价，为基于类型的优化与重构提供证明，并构造逻辑关系模型。
量子 λ-演算的完全抽象
为量子 λ-演算的博弈语义建立完全抽象，并证明量子关系模型也完全抽象。
数据打包的高效参数化算法
首次给出数据打包问题的参数化算法与细粒度二分，基于访问超图树宽实现线性时间求解。
高阶多态、存在类型与索引类型的可靠且完备的双向类型检查
基于聚焦（focalization）给出支持高阶多态、存在类型与索引类型（GADT）的双向类型检查声明式规范与算法规则，并证明其可靠完备。
面向安全性证明的归约
提出基于程序上下文的两类可靠程序归约，利用步骤可交换性简化并发程序安全性证明与自动验证。
模块化定量监控
提出数据转换器模型以实现流数据查询的模块化编译，并定义 QRE-Past 定量监控语言。
嵌套并行程序中的解纠缠
提出嵌套并行程序的内存性质“解纠缠”，并据此设计内存管理技术以提升效率与可扩展性。
绑定作为有界自然函子
提出用有界自然函子统一建模带绑定语法，并在 Isabelle/HOL 中形式化自由变量、α-等价与捕获避免替换等原理。
同一枚硬币的两面：会话类型与博弈语义——同步的一面与异步的一面
为同步会话π演算建立基于事件结构的博弈语义，实现完全抽象解释与同步/异步策略编码。
从细粒度到粗粒度动态信息流控制及其反向
证明细粒度与粗粒度动态信息流控制表达能力等价，并给出语义保持的双向翻译。
双模拟作为守卫递归类型的路径类型
在 Ticked Cubical Type Theory 中证明，任意函子的终守卫余代数的双模拟等价于路径相等。
SyTeCi：自动化带引用的高阶程序的上下文等价
将带局部整数引用的高阶程序上下文等价归约为内存配置迁移系统的不可达性，并用约束 Horn 子句自动判定。
Spy game：在 Iris 中验证局部通用求解器
在 Iris 中验证局部通用求解器的部分正确性，证明其虽用可变状态记忆与窥探，外部行为仍纯且计算最优最小不动点。
Taylor 涵摄 Scott、Berry、Kahn 与 Plotkin
用 Taylor 展开的资源敏感理论，统一并简化 λ 演算中原本依赖 Scott、Berry 与 Kahn–Plotkin 理论的重要证明。
标签依赖的会话类型
提出标签依赖会话类型，将通信与数据引入/消去解耦，并支持类型级原始递归。
路径依赖类型的可判定子类型
为 Wyvern 定义两种路径依赖类型变体，实现可判定类型检查并给出机器验证证明。
基于幽灵监视器的演绎验证
提出幽灵监视器辅助程序，将目标程序验证归约为监视器验证，并支持无穷行为。
渐进类型中哪些问题是可判定的？
该论文研究渐进类型迁移空间的关键可判定性，给出三种算法并证明判定极大元存在性为 NP 难。
模态、凝聚与信息流
用 classified sets 范畴和 Lawvere 凝聚理论，为模态类型控制信息流建立语义并证明非干涉定理。
Esterel 的一个演算：能则能，不能则不能
提出首个 Esterel 等式演算，支持源码级等式重写推理程序行为，并帮助发现实现缺陷。
作为宏的依赖类型系统
提出 Turnstile+：用宏实现依赖类型系统的高层元 DSL，支持快速原型化依赖类型语言与证明助手扩展。
带内存回收的无锁数据结构的指针生命周期类型
提出指针生命周期类型系统，检查无锁数据结构对 SMR 内存的安全管理，并自动推断类型与不变量以验证线性一致。
归责转移有效吗？
提出经验方法评估契约系统中归责信息能否系统定位缺陷，并用其分析 Racket 契约系统。
从线性时序规约合成协调程序
首次针对任意 LTL 规约，从多智能体环境合成能处理非确定性与隐藏动作的协调进程。
带方差的参数多态对称多重分派
首次形式化支持对称多重分派、多重继承和带方差参数多态的对象语言，并证明其类型可靠性。
Familial monads 与结构化操作语义
提出 familial monad 范畴框架，统一结构化操作语义，并证明互模拟同余与上下文互模拟可靠性。
数据类型声明的 kind 推断
系统研究数据类型声明的 kind 推断，为 Haskell98 与 PolyKinds 给出声明式及算法化规范并证明其性质。
归约单子及其签名
提出归约单子与归约签名，统一代数地呈现λ演算等系统的替换结构与有向归约规则。
对称 data 与 codata 的分解多样性
提出支持 data/codata 对称分解并可自动互译的语言，给出机器化验证与 IDE 实现。
PλωNK：函数式概率 NetKAT
提出函数式概率网络语言 PλωNK，以高阶抽象和 ωQBS 语义扩展 Probabilistic NetKAT。
部分类型构造子：或，让特设数据类型不那么特设
提出部分类型构造子的语言设计与形式理论，用限定类型刻画其定义域，支持部分数据类型作为一等公民。
弱按值调用 λ-演算在时间和空间上都是合理的
证明弱按值调用 λ-演算的 β-归约步数与最大项大小是合理的时间、空间度量，可与图灵机多项式时间、常数空间互模拟。
维度界下的主类型性与近似
为带维度界的交类型演算建立主类型性的代数与算法理论，并实现无需 β-归约的近似范式计算。
假装同步：异步分布式程序的同步验证
提出“假装同步”方法，将异步分布式程序同步化为等价赋值程序，用Floyd-Hoare验证条件与SMT进行验证。
不依赖 K 的定义性证明无关性
提出一种在保持类型检查可判定且与 univalence 兼容的前提下，为类型论加入定义性证明无关性的通用方法。
图解代数：从线性系统到并发系统
提出资源演算，一种图表式并发语言，用自然数替换信号流演算中的实数，并以等式理论刻画其可定义行为。
白天作绑定器，夜晚作标签：经由词法作用域 handler 实现效应实例
提出用词法作用域 handler 为代数效应实例命名并在类型中追踪，从而在同一上下文中组合同一效应的多次使用。
构造商归纳-归纳类型
通过签名理论构造有限QIIT，并证明其存在、依赖消去及与初始代数等价
迟来总比不来好：经典进程的完全抽象语义
提出 HCP，将线性逻辑扩展到超环境，从证明重写提取 LTS，并证明双相似、指称等价与带杠同余重合。
抽象化代数效应
提出 λ_HEL 演算及存在/局部代数效应，用类型化运行时强制转换保障效应抽象不被破坏。
抽象可扩展数据类型：或，行类型无论何名
提出 row theories 与 qualified types，统一抽象可扩展记录和变体，并保持 coherence 与主类型。
渐进 Hindley–Milner 类型化的动态类型推断
提出中间语言 λBDTI，将静态推断未定的类型变量推迟到运行时实例化，避免翻译发散并证明渐进保证。
博弈语义中调度与同步的范畴组合学
提出用同步模板与范畴组合学统一刻画博弈语义中可组合的调度策略，并构造交替与非交替线性逻辑博弈模型。
完全抽象的模块编译
提出首个具有动态正确性定理的模块编译翻译，证明其完全抽象并保持源语言抽象性。
π 演算中的交集类型与运行时错误
提出基于非幂等交集类型的 π 演算类型系统，刻画无运行时错误且可“完成工作”的进程，并证明其完备性。
渐进参数性再探
提出渐进参数多态语言 GSF，给出设计、元理论与参考实现，并证明动态渐进保证与参数性不相容。
Par 意味着并行：乘法线性逻辑证明作为并发函数式程序
将乘法线性逻辑证明解释为并发函数式程序的类型系统，并证明 λpar 的元理论性质。