TOPLAS（CCF A）（共 199 篇）
202621 篇 · 48(2)
通过对局部推理错误的反馈引导基于 LLM 的循环不变式合成
通过形式化验证 LLM 的推理步骤并定位局部逻辑错误，为其循环不变式合成提供建设性反馈，显著提升成功率。
在云上扩展过程间数据流分析
提出分布式框架 BigDataflow，用分布式 worklist 算法在集群上高效完成百万行级程序的过程间数据流分析。
Project Everest：开发工业级高保障软件的视角
回顾 Project Everest 近十年用程序验证构建工业级高保障安全通信软件的经验与得失。
Cut-Shortcut 全程序指针分析：重新构想无需上下文的上下文敏感分析
提出 Cut-Shortcut，无需上下文即可在指针流图中裁剪不精确边并添加跨方法捷径边，实现快速且精确的 Java 指针分析。
Coma：一种具有显式抽象屏障的中间验证语言
提出中间验证语言 Coma，用显式抽象屏障分离接口与实现，并生成正确且更紧凑的验证条件。
基于指称语义的组合式编译器验证
提出基于指称语义与行为精化的编译器验证框架，通过语义链接和精化代数实现从子语句、函数到模块及整程序的组合验证。
StreamAlloc：一个用于分析与变换 CUDA 代码以实现异步执行的框架
提出 sync2async 优化与 StreamAlloc 数据流分析框架，自动为 CUDA 同步传输与内核分配流并插入同步，在保持依赖的前提下最大化并行。
面向动态语言的类型化中间表示
提出类型化高层 IR，显式表达动态语言特性并支持特化、内联、作用域与拷贝消除等优化。
SQL 引擎中类型与类型转换语义的形式化框架
提出 TRAF：一种刻画 SQL 静态与动态类型及隐式类型转换的形式化类型语义框架，并给出类型安全条件与五引擎实例化验证。
VyZX：图形量子语言的形式化验证
提出 VyZX 库，用归纳图在证明助手中形式化验证 ZX 演算的图示重写规则及其可靠性。
面向安全货币流的可靠类型系统
为 TinySol 智能合约提出可同时保证调用完整性与非干涉的安全货币流类型系统。
ML 的全向类型推断：无论如何保持主类型性
提出全向类型推断，通过可挂起约束与增量实例化在 let-泛化下恢复 ML 扩展的主类型性。
用性能分析器导航混合类型迁移
评估现成性能分析器能否指导 Typed Racket 的逐组件混合类型迁移，并给出最有效的边界分析器驱动迁移策略。
宽松硬件架构上计算机程序设计的公理基础：AxSL 逻辑族
提出 AxSL 分离逻辑族，为 Arm-A 等宽松内存模型提供模块化 Hoare 式推理，并在 Iris 中机器化证明其可靠性。
带共享溯因与双溯因循环加速的组合式形状分析
提出共享溯因与双溯因循环加速，使基于双溯因的形状分析更精确、更高效且单阶段健全。
课堂中的形式化自动评分（扩展版）
将程序验证器用于本科编程课自动评分，通过等价性检查评估学生提交并区分递归结构。
异步二元会话的公平终止
提出公平异步子类型并在线性逻辑中构建会话类型系统，保证良类型进程公平终止且无饥饿与孤儿消息。
异步 must-前序的构造性刻画
证明在异步通信下，增强服务器为转发器后 must-前序的标准刻画仍成立，并在 Rocq 中机械化。
线性会话抽象机
提出 Linear SAM：面向对应 CLL 的会话类型程序的确定性顺序抽象机，并证明其与 CLL 证明归约相互对应。
用相继式演算编译
提出以相继式演算贯穿全程的编译器，支持控制效应与 data/codata 混合求值，可生成机器码。
TOPLAS ACM Transactions on Programming Languages and Systems2026引用 1
202520 篇 · 47(3)
C 语言的健全静态数据竞争验证：这场竞争输了吗？
通过真实程序基准与代码惯用法微基准，揭示健全静态数据竞争验证工具的能力、局限与不健全性。
结果逻辑：带分支效应的程序逻辑元理论的统一方法
提出 Outcome Logic，将分支效应置于核心，统一多种带分支效果的程序逻辑并给出相对完备证明系统。
基于效应类型与线性依赖的电路宽度估计
提出 Proto-Quipper-R，用线性依赖类型与效应系统推导电路宽度参数上界，并实现 QuRA 工具验证。
基于半定规划的多项式程序不变式合成
用半定规划松弛与鲁棒优化合成多项式程序不变式，分别求解强、弱不变式合成问题并给出理论保证。
Trocq：超越等价与 univalence 的免费证明转移
提出 Trocq 证明转移框架，基于新的类型等价表述推广 univalent parametricity，并实现为 Coq 插件。
可扩展语言元理论推理的模块化方法
提出可扩展语言的模块化元理论方法，按语言片段分解证明并对扩展做通用推理，并实现于 Sterling/Extensibella。
观测等价遇上 CIC
提出类型强制转换算子，使观测等价与 CIC 的索引归纳类型兼容，并在 Coq 中实现。
依赖类型理论的通用双向类型系统
提出依赖类型理论的通用双向类型化框架，证明其与声明系统等价并在规范化时给出可判定算法。
CFLOBDD 相对于 BDD 的多项式界
证明相同变量序下 CFLOBDD 规模至多比 BDD 多项式的倍，且该界在立方下界意义下是紧的。
装得下吗？验证垃圾回收下并发程序的堆空间上界
提出 IrisFit 分离逻辑，用空间信用在 Coq 中验证带追踪 GC 的并发程序最坏情况堆空间上界及安全/活性。
面向 Release/Acquire 并发的 Brookes 风格指称语义
首次在 Moggi 单子框架下为 RA 弱内存模型的函数式并发语言给出组合式指称语义，并验证程序变换。
单子交集类型：关系式与有序式
将交集类型提升到带代数效应的计算演算，并用单子与前序语义刻画程序观察行为。
面向 WAR 感知间歇计算的模态崩溃类型
提出崩溃类型系统与模态逻辑基础，用于建模并证明间歇计算中检查点与重执行的正确性。
面向 IoT 系统的基于速率的会话类型
提出基于速率的会话类型与速率兼容性，确保 IoT 消息传递速率一致，并在 Rust 中实现原型。
作用域效应、作用域操作与参数化代数理论
将作用域效应翻译为参数化代数理论的变体，给出等式推理与用生成元和方程刻画 monad 的新方法。
通过合并实现动态继承的类型安全编译
为支持动态继承的静态类型语言 CP 设计类型安全编译方案，并优化合并操作性能。
TOPLAS 的季节更替
这是一篇关于 TOPLAS 期刊编辑更替的社论，无研究内容。
编者按：新年，新论文轨道
主编就任编者按，宣布期刊新年新增论文轨道，并感谢离任主编。
202415 篇 · 46(2)
抽象解释中的对抗性：用抽象解释容纳鲁棒性
用抽象解释将分类误差建模为抽象，定义并刻画弱化鲁棒性及其对抗边界。
CFLOBDDs：上下文无关语言有序二元决策图
提出 CFLOBDD，一种可替代 BDD 的布尔函数压缩表示，最佳情况下比 BDD 指数级更小、比决策树双指数级更小。
下近似抽象域设计的局限与困难
论文证明基于下近似 Galois 连接的抽象域在常见传递函数下难以进行非平凡的错误查找分析。
基于按需摘要的交互式抽象解释
提出按需摘要，首个在任意抽象域中保证从零一致性的增量组合式静态分析算法。
LoRe：一种用于可验证安全本地优先软件的编程模型
提出 LoRe 编程模型与编译器，自动验证 local-first 应用的安全性质，并按需引入强一致性协调。
Homeostasis：自稳定编译器的设计与实现
提出自稳定编译器框架 Homeostasis，自动捕获变换并触发程序抽象稳定化，免去遍写者手动处理。
Gradual C0：用于渐进验证的符号执行
首个实用递归堆数据结构渐进验证器 Gradual C0，用符号执行减少动态检查开销。
证明转移系统模型的并行实现正确性
提出基于模拟关系的方法，证明 actor/active object 并行实现相对于转移系统规范的正确性。
并发编程语言的局部抽象、全局具体语义
提出模块化并发语言语义，将局部抽象求值与全局具体组合分离，以声明式刻画并发模型并支持程序逻辑。
基于多维同态的数据并行计算（解/重）组合
提出基于多维同态的形式化分解/重组方法，可自动生成并调优数据并行代码。
基于分解的合成：应用分治类算法范式
提出 AutoLifter，通过分解方法消除语法限制，自动将分治类算法范式应用于程序合成。
类型论中内涵分析的分层方法
提出分层模态类型论，以统一语法分离代码表示与计算，支持元编程和内涵分析。
通用可组合性即鲁棒编译
证明通用可组合性（UC）与鲁棒编译（RC）之间的形式联系，并用 DEEPSEC 机械化 UC 协议证明。
Choral：面向对象的编排编程
提出首个面向对象编排编程语言 Choral，将编排编译为各角色的纯 Java 库以实现模块化分布式开发。
TeraHeap：利用闪存存储缓解托管大数据框架中的 DRAM 压力
TeraHeap 通过扩展 JVM 在闪存上建立第二堆，消除大数据框架对象的序列化/反序列化与 GC 扫描开销，缓解 DRAM 压力。
202321 篇 · 45(2)
Passport：利用标识符改进自动形式化验证
为证明合成模型的标识符引入类别词汇索引、子词序列建模与路径细化三种编码，自动证明的定理数最多提升 29%–45%。
面向 SC、TSO 和 PSO 内存模型的模序一致性理论可满足性
提出适用于 SC、TSO 和 PSO 内存模型的序一致性理论及 SMT 求解器 Zord，显著提升并发程序验证性能。
面向运算符优先级语言的模型检测器
提出并实现了首个开源模型检测器 POMC，用于验证运算符优先级语言程序上的 POTL 树结构性质。
有类型–无类型交互：比较分析
提出统一评估框架，对比若干主流有类型–无类型交互语义，帮助设计者分析自身动态语义的保证。
带 Frame 的一阶逻辑
提出 Frame Logic，扩展一阶逻辑与递归定义，用支持集实现 frame reasoning，并用于堆程序局部规范。
捕获类型
提出在类型中紧凑记录值所捕获自由变量的演算 CC<:□，并用于安全实现作用域能力与效应多态。
SSProve：在 Coq 中面向模块化密码证明的基础性框架
提出首个在 Coq 中机器检验状态分离密码证明的通用框架 SSProve，结合模块化证明与概率关系程序逻辑。
Omnisemantics：非确定性的平滑处理
提出 omni-big-step 与 omni-small-step 语义，用「状态到结果集合」的推导统一刻画非确定性与未定义行为，并内蕴安全性。
面向差分隐私的上下文线性类型
提出 Jazz：用线性类型与潜在上下文效应支持高阶程序及高级差分隐私变体的语言与类型系统。
通过部分控制流线性化消除侧信道
将部分控制流线性化用于安全，使程序执行路径不依赖秘密，从而消除时序侧信道。
优化感知的编译器级事件剖析
提出在编译器内部、推迟至优化之后插桩的事件剖析技术，降低剖析对编译优化的扰动，并在 Graal 上验证。
面向操作系统移植的程序合成
用两个 DSL 与符号执行合成引擎自动生成操作系统的机器相关汇编代码，实现 OS 移植。
多输入解析与词法分析
提出通用解析扩展 MGLL，支持高效同时解析多个输入串，并据此增强词法分析，兼顾字符级与 LEX/YACC 风格。
利用部分上下文敏感的剖析信息提升热代码性能
提出基于部分上下文敏感 profile 的热区重建与编译预算分配技术，在 GraalVM Native Image 中提升热代码性能并控制代码膨胀。
面向健全的面向对象信息流控制的不可变性与封装
提出面向对象语言 SIFO，用不可变性与唯一性类型修饰符提升信息流控制精度，证明非干扰性并实现为可插拔类型系统。
通过程序合成与时间受限穷举搜索优化同态求值电路
提出自动学习重写规则并利用时间受限穷举搜索优化 FHE 电路的方法，降低乘法深度。
聚焦精化类型
用聚焦证明论方法为精化类型系统建立可判定、可靠且完备的 SMT 约束生成基础。
一种基于导数的可见下推文法解析器生成器
提出基于导数的可见下推文法解析器生成器，线性时间产出并提取全部歧义解析树，核心算法在 Coq 中验证。
Prisma：一种用于在去中心化应用中强制合约-客户端协议的无层语言
提出无层语言 Prisma，将合约与客户端统一编写，用 direct-style 通信原语保证接口协议一致。
面向多核的 ForeC 同步确定性并行编程
提出同步多线程语言 ForeC，用共享变量语义实现多核嵌入式程序的确定性并行、无死锁与静态时序分析。
有限列表上龟兔算法的组合式方法
为有限列表上的龟兔算法给出组合式解释，并用 OCaml 与 Coq 形式化验证回文检测器。
202222 篇 · 44(2)
面向 Interleaved-Dyck 可达性的快速图简化
提出一种与具体 InterDyck 可达性算法正交的图预处理简化方法，安全删除不贡献交错 Dyck 路径的边，提升精度与可扩展性。
TF-Coder：面向张量操作的程序合成
提出 TF-Coder，用带模型引导的自底向上加权枚举搜索，从输入输出示例合成 TensorFlow 张量操作代码。
CHAD：组合子同态自动微分
提出 CHAD，一种纯函数式、类型保持且可证明正确的前向/反向自动微分源到源变换方法。
一种具有数据抽象和动态框架的关系程序逻辑
提出带动态分配对象语言的关系霍尔逻辑，以状态化框架条件统一封装、隐藏与实现耦合。
嵌套会话类型
为会话类型引入 prenex 多态与嵌套递归数据类型，证明类型等价可判定并提出高效可靠算法。
Armada：具有可靠语义可扩展性的并发代码自动验证
提出 Armada 语言与工具，借助 SMT 自动化和可扩展的可靠推理技术，低代价形式验证高性能并发程序。
强分离逻辑
提出强分离逻辑，通过限制分离合取的语义，在保留魔法棒和归纳谓词的同时恢复可判定性。
使用 Squeezers 的运行时复杂度上界
提出基于 squeezers 的迹比较方法，为现有代价分析难以处理的程序推导更紧的运行时上界。
因果一致共享内存的可判定性是什么？
本文证明两类因果一致共享内存下有限状态并发程序的安全性验证可判定，并给出基于有损操作语义的判定方法。
深入剖析 ZGC：OpenJDK 中的现代垃圾收集器
对 OpenJDK ZGC 做高层设计解析，并用 SPIN 模型解释 mutator 与 GC 线程的并发竞争及解决。
归纳构造演算（CIC）的渐进化
研究 CIC 的渐进化，揭示渐进性与归一化、宇宙封闭的权衡，并给出三种折中方案及其元理论。
让预言变量变得简单
提出一种更易使用的新型预言变量，并以更数学化的方式重新表述精化映射理论。
重新审视 iso-recursive 子类型
重新形式化 iso-recursive 子类型，提出基于双重展开的可靠、完备且可判定的算法规则并在 Coq 中验证。
为了多几美元：经验证的细粒度算法分析直至 LLVM
提出基于资源货币的逐步精化框架，在 LLVM IR 上验证高效算法的功能正确性与（摊还）最坏情况复杂度。
π-演算中并行计算复杂度的类型
为 π-演算提出两个类型系统，可从类型推导提取并行计算中 work 与 span 的复杂度界。
会话余代数：正则与上下文无关会话类型的余代数视角
用余代数给出会话类型的无语法语义，统一正则与上下文无关会话类型并导出可判定子类型系统。
消息传递并行程序的类型规约
提出 ParTypes 类型规约，为消息传递并行程序规定协议，并保证类型检查可判定、良类型程序无死锁且终止。
两种参数性与三种 Universal Type
揭示扩展 System F 因类型变量失去词法作用域而产生 universal type，并用类型世界修正参数性、否证两个猜想。
求解含大整数值的程序草图
提出基于中国剩余定理的求解技术，使 Sketch 的整数编码能高效处理大整数值程序草图。
无容器的多值：面向对象编程中数量与类型的分离
提出 OO 语言 Num，分离对象数量与类型，统一处理零/一/多对象，并用 plural method 取代静态方法。
有界抽象效应
提出一种支持抽象、聚合与上下界层级的效果系统，并集成到 Wyvern 语言中。
ESOP 2021 特刊导言
介绍 ESOP 2021 特刊的选文流程、扩展评审与收录论文主题。
202121 篇 · 44(1)
通过类型系统刻画条件独立性
提出信息流类型系统捕获概率模型的条件独立性，并用类型推断与程序变换自动消除离散参数。
RustHorn：基于 CHC 的 Rust 程序验证
提出将带指针与动态内存的 Rust 程序归约为 CHC 的新方法，利用权限保证消除指针和内存状态，并证明可靠性与完备性。
基于惰性顺序化的多线程程序有界验证
提出惰性顺序化，将有界多线程 C 程序转为串行程序，复用 BMC 高效验证并发。
CSim²：Isabelle/HOL 中基于 rely-guarantee 的并发系统组合式自顶向下验证框架
在 Isabelle/HOL 中提出组合式 rely-guarantee 仿真框架 CSim²，将并发系统高层规约的性质自顶向下保持到实现层。
随机程序中用于可达性的秩上鞅与排斥上鞅
为随机程序可达概率的上/下近似统一基于鞅的方法，并提出秩上鞅与排斥上鞅两类新技术。
重新审视 Zones 与 Octagons
提出基于改进图数据结构与算法的 Zones 和 Octagons 抽象域快速实现，显著提升静态分析性能与验证效果。
一种带精度估计的数据隐私编程语言
提出 DPella 编程框架，静态追踪差分隐私数据分析的精度及其与隐私的权衡。
基于抽象解释的责任分析的系统化设计
提出基于抽象解释的责任分析，用迹语义抽象定义责任，并给出可靠的抽象分析框架。
论时间敏感的控制依赖
提出时间敏感控制依赖的高效算法，并用于发现缓存计时泄漏。
武装的猫：Arm 一致性模型的形式化建模
综述 Arm 用 cat 语言形式化并发一致性模型的工作，含混合大小访问扩展、等价表述及 x86 验证。
Rust 中引用生命周期与借用的轻量级形式化
提出流敏感轻量级类型系统与演算，统一形式化 Rust 的引用生命周期和借用安全。
多态可迭代顺序效应系统
提出以 effect quantale 为参数的抽象多态顺序效应系统，并推导出尽可能精确的迭代结构。
TaDA Live：细粒度并发程序终止性的组合推理
提出 TaDA Live 并发分离逻辑，以活性假设和分层主观义务组合推理细粒度并发程序终止性。
轨迹相关编译正确性与安全编译的扩展论述
用任意源—目标轨迹关系泛化编译正确性，刻画源与目标轨迹性质的双向保证，统一涵盖未定义行为、侧信道与安全编译。
鲁棒安全编译（RSC）：一种高效的安全编译形式
提出鲁棒安全编译（RSC）作为完全抽象编译的替代准则，更易证明且生成代码往往更高效。
保障小型微处理器上可中断的 enclave 执行安全
提出以完全抽象作为处理器扩展安全性的形式化准则，设计、证明并实现可中断 enclave，评估其性能与硬件开销。
论多态会话与函数
建立多态会话π演算与线性System F之间互逆且完全抽象的编码，并由函数理论导出会话类型结果。
现代编程语言的安全默认并发
提出 volatile-by-default 并发语义，使安全语言默认顺序一致，并允许通过注解按需放弃以保证性能。
Hoare 逻辑中按值调用推理的完备性与复杂度
提出首个针对含局部变量和按值调用参数机制的递归过程偏正确性的可靠且相对完备 Hoare 逻辑，证明长度与程序规模成线性。
ESOP 2020 专题导言
介绍 ESOP 2020 特刊背景，并概述两篇受邀扩展论文：安全编译与 Rust 验证。
组合式编程（Compositional Programming）
提出静态类型的组合式编程风格与 CP 语言，用组合式接口、trait、方法模式等概念同时解决表达式问题与模块化依赖。
202014 篇 · 42(2)
多种基测度下的符号化分解
提出首个支持可变基测度的符号化测度分解变换，可检查或推断基测度，并在语义上证明其可靠性。
命令式概率程序的切片理论
提出命令式概率程序的切片理论，给出语法条件、语义正确性证明与最小切片算法。
推断整数程序的运行时下界
提出一种可处理非尾递归的整数程序最坏情况运行时下界推断技术，并在工具 LoAT 中实现。
广义 points-to 图
提出广义 points-to 图（GPG），用紧凑的自底向上过程摘要实现精确且可扩展的指向分析。
指针分析中选择性上下文敏感的一种原则性方法
提出基于值流模式的ZIPPER算法，选择性应用上下文敏感，在指针分析中兼顾精度与速度。
Obsidian：面向智能合约的安全编程语言
提出 Obsidian 语言及其核心演算 Silica，用 typestate 与线性类型静态检测智能合约常见漏洞，并证明类型可靠性。
调试大规模 Datalog
提出可扩展的自底向上 Datalog 溯源调试策略与定点语义，并集成到 Soufflé 高效实现。
C 语言的类型推断
提出基于合一的类型推断框架，恢复 C 程序中缺失的 struct、union、enum 与 typedef 声明，用于重建部分程序。
主动学习用于访问数据库应用的推断与再生成
提出 Konure，用主动学习推断访问关系数据库的应用模型，并将模型再生成带安全检查的 Python 实现。
过程间、可能非终止程序中基于依赖切片的语义正确性
为过程间且可能非终止程序上的一类基于依赖的切片方法给出通用语义正确性证明。
使用观察序列的过程间上下文无界程序分析
提出观察序列验证范式，以允许的线程上下文切换数为资源参数，实现可证明上下文无界安全性的过程间并发程序可达性分析。
PolyMage 的有效融合与 tile 大小模型
提出面向图像处理 DSL 的融合与 tile 尺寸模型，用动态规划优化循环嵌套融合，显著提升性能。
Chocola：统一 futures、transactions 与 actors 的并发语言
提出统一 futures、transactions 与 actors 的并发语言 Chocola，形式化语义并证明其保证。
勘误：Toro 等人的《带引用的类型驱动渐进安全》，ACM Transactions on Programming Languages and Systems (TOPLAS) 第 40 卷第 4 期，文章号 16
对《带引用的类型驱动渐进安全》一文的勘误，未提供摘要或新研究内容。
201925 篇 · 41(1)
重新审视增量式与并行指针分析
提出增量且并行的指针分析算法 IPA，避免冗余计算与图可达性分析，在保持精度同时实现大幅加速。
面向数据驱动程序分析的带析取模型的机器学习算法
提出带析取布尔模型的机器学习算法，自动学习数据驱动程序分析策略，显著优于手工调优。
常量树宽基本 RSM 中动态代数查询的更快算法
提出在常量树宽递归状态机上支持代数路径性质多次查询的轻量预处理算法，并显著加速按需过程间数据流分析。
Java 中注入攻击的静态识别
提出基于抽象解释的统一健全分析，静态识别 Java 中七类注入攻击的污点数据流。
递归程序的非多项式最坏情况分析
提出 measure function 及非多项式综合方法，证明非确定性递归程序非多项式最坏情况界。
模块化乘积程序
提出模块化乘积程序，将超属性验证模块化，并在 Viper 中验证信息流安全等性质。
基于单子仿射大小类型的概率终止
提出单子仿射大小类型系统，可类型化概率高阶程序并证明其几乎必然终止。
PYE：精确且高效的两步（静态+JIT）分析框架
提出 PYE 两步分析框架，静态编译生成条件值、JIT 阶段解析条件，实现精确且低开销的运行时分析。
高阶需求驱动程序分析
提出高阶需求驱动程序分析 DDPA，将需求驱动查找扩展到高阶程序，保持流/上下文敏感与多项式复杂度。
基于约束求解的 CSS 最小化
将 CSS 规则合并最小化归约为 CSS 图优化，并用 SMT/Max-SAT 求解，实现语义保持的压缩。
概率高阶语言的环境互模拟
为概率高阶语言定义环境互模拟，并证明其相对于上下文前序与上下文等价的全抽象性。
组合寄存器分配与指令调度
提出基于约束编程的组合优化方法，统一求解寄存器分配与指令调度，生成优于 LLVM 的可执行代码。
Resilient X10 中的故障恢复
将 Resilient X10 从故障感知推进到故障恢复，把冗余与恢复负担转移给运行时与标准库，降低程序员负担。
对带局部能力（local capabilities）的机器进行推理
为带局部能力的能力机器建立逻辑关系，证明控制流正确性与局部状态封装。
面向所有的一致子类型
提出适用于多态子类型的一致子类型推广定义，并构建支持隐式高阶多态的渐进类型演算。
Curry 风格语言的实用子类型系统
提出面向 Curry 风格语言的语法导向子类型框架，用带大小不变量的（余）归纳类型证明递归程序终止。
垃圾回收（GC）时机的最优选择
将程序特定的 GC 调度形式化为优化问题，用动态规划求非分代与分代 GC 的最优回收时机。
ML、可见下推类内存自动机与带状态的扩展分支向量加法系统
证明 ML 有穷片段的可观察等价问题递归等价于 EBVASS 可达性，并用 VPCMA 给出自动机刻画。
论编程语言对代码质量的影响
复现并再分析2014年研究，揭示编程语言与缺陷的关联被严重高估，仅4种语言显著且效应极小。
上下文无关会话类型推断
提出面向 context-free session types 的语法导向类型系统，并用两个 OCaml 嵌入实现检查与推断。
通过模态刻画代数效应的行为等价
提出用模态逻辑刻画代数效应程序行为等价的一般框架，并证明其与applicative bisimilarity一致且为同余。
Java虚拟机上的任务粒度分析与优化
提出低开销任务粒度剖析方法，揭示JVM任务并行瓶颈，并通过优化任务粒度获得最高5.90倍加速。
一个带依赖类型的经典相继式演算
给出带控制算子和依赖类型的 call-by-value 语言的相继式演算，并用 CPS 翻译证明其可靠性。
ESOP 2018 特刊导言
ESOP 2018 特刊的导言；摘要缺失，无法概括具体研究贡献。
编者按
该条目为编者按，无摘要，无法概括编程语言领域的具体研究贡献。
201820 篇 · 41(1)
使用符号泰勒展开严格估计浮点舍入误差
提出符号泰勒展开方法并实现 FPTaylor，用严格全局优化更紧致地估计浮点最大舍入误差。
概率编程中的条件化
在 pGCL 上研究 conditioning 的 wp 与操作语义，证明其对应条件期望奖励，并给出消除 conditioning 的程序变换。
通过贝叶斯优化学习实现自适应静态分析
提出用贝叶斯优化从代码库学习参数化分析策略，实现按需流/上下文敏感的自适应静态分析。
抽象解释框架中敏感性的理论基础
在抽象解释中提出统一描述上下文、调用点、对象等各类敏感性技术的通用抽象域构造框架。
用于程序分析的程序合成
提出以程序合成为统一机制的静态分析框架，并用受限二阶逻辑片段建模多种验证任务。
非确定性程序与系统的静态后向切片
提出非确定性程序图上的后向切片理论，用 commitment 封闭刻画弱/强切片并给出 O(n^3) 算法。
对《非确定性程序与系统的静态后向切片》的编辑前言
编辑前言，引出非确定性程序与系统的静态后向切片这一主题。
仿射概率程序定性与定量终止问题的算法分析
本文用线性 ranking supermartingale 合成，对仿射概率程序的终止性定性与定量问题给出算法及复杂度界。
常数树宽组件并发系统中的代数路径性质算法
为常数树宽组件的并发系统提出代数路径性质查询算法，实现预处理与查询时间权衡并改进最坏情况复杂度。
基于约束的重构
将基于约束的重构从类型推广到名称、位置、可访问性等属性，并给出工具正确性条件与实现算法。
含纯方法调用规约的框架推理逻辑分析
将纯方法与读效应引入区域逻辑，为模块化框架推理建立可靠证明规则并机器检验示例。
单线程与多线程程序的模块化终止性验证
提出一种模块化规约与验证方法，用方法名多重集等层级表达式证明面向对象程序（含堆修改与并发）的终止性与活性。
通用屏障同步的动态死锁验证
提出 Armus：基于 phaser 的事件图模型，为 X10 与 Java 实现可靠完备的动态屏障死锁检测与避免。
面向语言特性的性能剖析
提出特性特定剖析，按语言构造报告性能开销，帮助程序员定位特定语言特性的昂贵使用。
基于会话的逻辑进程的互连能力
证明经典线性逻辑的会话式进程组合在互连网络上弱于多党会话演算，并提出保持无死锁的循环互连组合规则。
面向患者的处方编程语言（POP-PL）
设计并评估面向患者的处方编程语言 POP-PL，使部分医疗处方可被形式化表达并由临床医生理解修改。
类型驱动的带引用渐进安全
提出带引用的高阶渐进安全类型语言 GSL_Ref，仅靠类型标注统一静态与动态安全检查，并支持对所有程序进行静态非干涉推理。
多语言运行时中的跨语言互操作性
提出 TruffleVM 与 generic access 机制，实现多语言运行时中高效无缝的跨语言互操作。
事务性 Sapphire
实现并评估 Jikes RVM 上首个 on-the-fly 并行复制式 GC Sapphire，借助硬/软件事务与模型检验保证正确性。
对 Grimmer 等人《多语言运行时中的跨语言互操作性》的勘误
这是一则勘误，更正 Grimmer 等人关于多语言运行时跨语言互操作性的原文。
201720 篇 · 39(2)
面向实数的编译器
提出源到源编译器Rosa，可根据误差规约将实数程序自动合成浮点或定点代码，并统一估计舍入误差。
SHErrLoc：定位静态分析检测到的程序员错误
提出基于约束不可满足性和贝叶斯解释的通用错误定位方法，并实现工具 SHErrLoc。
从清晰到高效：面向分布式算法
提出一种高层分布式算法语言及自动优化，将复杂同步条件转为增量更新，从而高效实现逻辑量化。
静态分析告警的健全非统计聚类
提出基于可靠依赖的静态分析告警健全聚类，若簇主导告警为假则同簇其余告警必假，减少45%告警报告。
位精确的过程模块化终止性分析
提出面向C程序的位精确过程模块化终止性分析，通过模板化过程间摘要结合前向过近似与终止前置条件欠近似推断。
Typestate 导向编程的化学方法
提出基于化学隐喻的 typestate 导向编程，以消息分子和化学反应建模并发状态变换，并用行为类型控制对象协议与共享。
使用 Hyperball 抽象域验证可靠性属性
提出 Hyperball 抽象域及 Scale 析取精化，用抽象解释量化软错误位翻转导致的最坏语义偏差。
不要坐在栅栏上
提出面向大型代码库的内存栅栏自动放置技术，以精度换可扩展性，并实现为 musketeer 工具。
精确预测分析：发现 MPI 程序中的通信死锁
提出基于偏序与命题编码的 MPI 通信死锁预测分析方法，并实现 MOPPER 工具，可扩展地检测单路径程序死锁。
用 Rely-Guarantee 与精化类型验证无锁数据结构的不变式
提出将 Rely-Guarantee 推理应用于引用，并用精化类型在未验证与完全验证之间验证无锁数据结构不变式。
一个简单、或许正确的C11 LR解析器
提出一个简单且接近C11标准的LALR(1)解析器，用词法反馈与作用域处理解决歧义。
基于张量积的牛顿式程序分析
提出基于张量积的改进技术，求解牛顿式过程间数据流分析中由非交换乘法产生的线性上下文无关语言子问题，并用于谓词抽象。
从证明生成程序（Programs from Proofs）
提出 PfP 框架，将安全证明转化为易检查程序，使消费者能快速验证不可信代码的安全性。
论子类型关系完备性，及其在等递归类型中的应用
提出证明子类型关系相对于类型安全完备性的方法，证明 Amber 规则不完备，并给出可靠完备且 O(mn) 的等递归子类型算法。
带异常的动态信息流中的多面值机制
提出多面值机制，为动态信息流控制提供避免卡死执行的终止不敏感非干涉保障，并处理异常、解密与许可。
多态 Manifest 契约：修订与解决
提出首个不依赖猜想、支持关系参数性的多态 manifest 契约演算，并以延迟替换解决既有类型转换关系的缺陷。
SPL：Streams 处理语言
设计并实现兼具分布式执行与可扩展性的流处理语言 SPL，成为 IBM Streams 平台的入口。
可靠地扩展
研究 Erlang 分布式 actor 模型的可扩展性瓶颈，在 VM、语言库与工具层改进，并在 256 主机集群验证可靠扩展。
部分压缩的局限性
扩展部分堆压缩的理论限制，给出更优且对现代托管运行时更有意义的界限。