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
标签：语言设计与特性（共 245 篇，按优先级展示前 200）
不完整程序的统计类型推断
提出两阶段方法 Stir，用神经网络预测 token 类型标签并还原复杂类型，将类型推断转化为序列到图解析问题。
Roulette：一种表达力强、精确且高效的离散概率编程语言
提出 Roulette，首个兼具高性能精确推断与通用语言特性的离散概率编程语言。
noDice：面向带非确定性与条件化的离散概率程序的推断
提出 noDice，扩展 Dice 以对含非确定性与条件化的离散概率程序进行推断，并用决策图缩减所构造 MDP 的状态空间。
Flix：一种语言集成 Datalog 的设计
提出 Flix 中语言集成 Datalog 的设计，使 Datalog 程序可模块化、多态、类型化地复用于程序分析等任务。
面向形式验证的元编程框架
在 Lean 中实现面向形式验证的元编程框架，通过反射对象级表达式支持高效编写 tactic 与自动化。
Mtac2：用于 Coq 中反向推理的类型化策略
提出 Mtac2，为 Coq 提供支持反向推理的类型化策略编程语言，可在策略定义期静态排除多类错误。
AI 程序员就在我们身边：面向高效代码生成重新思考编程语言文法
提出面向 AI 的编程语言文法概念，实现保持 AST 等价的 Python 方言 SimPy，减少 LLM 代码生成 token 用量 10% 以上。
用于组合式微分参数不连续性的分布
提出首个可靠微分参数不连续性的一阶可微语言 Potto，并给出指称语义与支持分离编译的高效实现。
多语言概率编程
提出 Multi PPL，使精确离散推断与重要性采样两种概率编程语言可靠互操作，并证明推断算法可靠性。
MTP：面向 AI 集成编程的意义类型化语言抽象
提出 MTP 范式，用语言级构造从代码语义自动生成提示并处理 LLM 输出，大幅降低开发复杂度。
嵌入 F* 的经过验证的低层编程
提出 Low*：将良行为 C 子集浅嵌入 F*，以类型保证内存安全并借助 F* 验证，经抽取编译到 C。
为什么正则表达式不是通用语言？关于正则表达式复用与可移植性的实证研究
通过对多语言正则语料库的实证分析，揭示正则表达式跨语言复用存在语义与性能差异及安全风险。
切入要点：pointful 数组编程的索引集与保持并行的自动微分
提出将数组视为类型化索引集上的函数，并用类型化效应支持可自动并行化原地更新及保持并行的反向自动微分。
SugarC：将真实世界 C 预处理器去糖为纯 C
设计并实现 SugarC，将真实 C 预处理器的编译期可变性去糖为纯 C 的运行时可变性，并同步类型检查。
Cedar：一种表达力强、快速、安全且可分析的授权语言
提出授权策略语言 Cedar，兼顾可读性、快速求值、安全与可分析性，并开源实现。
Java 动态代理的静态分析
以简洁逻辑规则在 Doop 中建模 Java 动态代理语义，使静态分析得以穿透代理层。
用效应处理器延续 WebAssembly
提出 WasmFX，用效应处理器为 WebAssembly 增加类型安全的续延与非局部控制流支持。
具有动态任务依赖的可扩展增量构建
提出一种增量构建算法，支持全功能编程语言脚本，执行代价随受影响任务数扩展而非项目规模。
Futhark 中高阶模块的静态解释：面向大规模的函数式 GPU 编程
为纯函数式数据并行语言 Futhark 设计高阶模块系统，并在 Coq 中形式化其静态语义与编译期消除。
Lower your guards：一个组合式的模式匹配覆盖检查器
提出 Lower Your Guards 算法，将模式匹配归约为守卫树，简化覆盖检查，并在 GHC 中实现，提升准确性和性能。
通过族多态实现可扩展的元理论机械化
提出基于族多态的语言设计，使证明助手能复用和扩展元理论机械化代码与证明。
在 Event-B 的 institution 中构建规约
为 Event-B 规约语言建立基于 institution 的形式语义，证明其满足性保持与模型合并条件，并统一参数化与精化等模块化构造。
基于关系扰动属性的增强示例合成
提出用关系扰动属性对示例合成施加语义偏置，自动增广示例以提升泛化能力。
实数及其他空间上的可计算决策
提出基于构造拓扑的程序语义，利用非确定性/部分性及空间模式匹配，在精确实数计算中实现可计算的离散决策。
用行为契约强化智能合约
提出 Solidity 语言扩展 ConSol，支持将行为契约附加到一等地址并在调用时监控违约，实现模块化的智能合约规约与验证。
轨迹契约
提出轨迹契约，用谓词约束多次函数调用与返回间的值序列，弥补传统行为契约表达力不足。
协变与逆变：对一个老问题的新审视（供函数式程序员学习的进阶类型系统入门）
重新审视面向对象方法参数的协变/逆变特化，论证二者可在同一语言中共存，并以实例讲解进阶类型系统概念与实现技巧。
“do”解缚：在纯函数式语言中拥抱局部命令式（函数式珍珠）
为纯函数式语言的 do 记法加入局部可变、提前返回与迭代，并给出到纯函数代码的翻译及 Lean 正确性证明。
黑盒设置下的增量上下文无关文法推断
提出 Kedavra，通过分段示例字符串并增量推断，提升黑盒上下文无关文法推断的质量、速度与可读性。
支持内涵分析的元编程依赖类型理论
提出 DeLaM 分层模态依赖类型理论，支持开放代码的引用、组合、递归分析与类型安全代码生成。
LoRe：一种用于可验证安全本地优先软件的编程模型
提出 LoRe 编程模型与编译器，自动验证 local-first 应用的安全性质，并按需引入强一致性协调。
极不合逻辑，Kirk：即便契约破损、类型不健全且 linter 过多，也能大规模发现类型不匹配
提出 Scotty，将 DefinitelyTyped 的类型声明转为契约并绑定到库与测试套件边界，通过运行测试检测类型与 JavaScript 代码的不匹配。
一种高效的类型安全结构化差异比较算法
提出一种线性时间、类型安全的数据类型泛型结构化 diff 算法，最大化共享并提升补丁自动合并率。
宏使用可移植性的语义分析
提出首个宏可移植性分析框架与工具 Maki，将宏行为分解为26个属性，以94%准确率识别易移植宏并指导C代码迁移。
C++ 开发者如何使用不可变性声明：一项实证研究
通过分析 7 个开源项目，实证揭示 C++ 开发者使用 const 表达不可变性的现状与漏标差距。
Coma：一种具有显式抽象屏障的中间验证语言
提出中间验证语言 Coma，用显式抽象屏障分离接口与实现，并生成正确且更紧凑的验证条件。
存在效应情况下的可替换性：一项大规模研究
对超 2000 万 Java 类的大规模分析表明，子类与超类方法在异常、同步、I/O 和方法调用效应上普遍不满足可替换性。
机会式并行 Lambda 演算
提出基于 lambda 演算的机会式求值策略，自动并行分派独立外部调用并流式返回结果，并用 Opal 语言验证。
黑盒环境下复杂编程语言的上下文无关文法推断
提出 Crucio，通过分解森林与分布矩阵从黑盒样本中为 C/C++/Java 等复杂语言高效推断上下文无关文法。
面向 ArkTS 的上下文敏感指针分析
提出首个面向 ArkTS 的上下文敏感指针分析框架 APAK，通过专用堆对象模型与插件架构提升调用图精度。
模块感知的上下文敏感指针分析
提出模块感知的上下文敏感指针分析，利用 JPMS 的 provides/uses 语义恢复指向关系并传播关键上下文。
迈向学习增强的编程语言
提出在现有编程语言中引入新特性，使开发者能直接利用现代强化学习算法与实现。
集合论类型在 Erlang 中的实践（经验报告）
将集合论类型检查器 Etylizer 应用于自身实现，实证其在真实 Erlang 代码中的表达力、可用性与可扩展性。
可扩展语言元理论推理的模块化方法
提出可扩展语言的模块化元理论方法，按语言片段分解证明并对扩展做通用推理，并实现于 Sterling/Extensibella。
认证编译器 à la carte
为 Rocq 引入晚绑定、mixin 组合与族多态的扩展机制（Rocqet 插件），使 CompCert 级别的认证编译器可模块化、可复用、按需组合。
命令式组合式编程：经双向类型化实现带可变引用的类型安全分配性交集子类型
用双向类型化仅限制引用规则，在保留分配性交集子类型的同时为组合式编程加入可变引用，并机器化验证类型安全。
灵活的正确性构造编程
提出并形式化两种更灵活的构造正确编程方法 CbC-Block 和 TraitCbC，并比较其可用性。
Async/Await 的设计空间探索
系统梳理 straight-line asynchrony 的九维设计空间，揭示看似相同的 async/await 在语义上的分歧。
使用可组合递归模式与变换进行编程
提出 CRPT：可组合递归模式与变换，将递归类型定义用于无回溯的线性时间识别与变换，并给出类型系统与实现。
当抽象违背物理：重新思考量子软件中的模块化设计
揭示量子软件中经典抽象与量子物理约束的根本冲突，并提出面向量子语义的安全抽象设计原则。
LARTS：面向实时与安全系统的语言抽象
提出 LARTS，用执行域、确定性内存契约与通信通道将实时、隔离与内存安全提升为可验证的语言抽象。
Iris-WasmFX：Wasm 栈切换的模块化推理
在 Rocq 中机械化 WasmFX 并证明类型可靠性，提出 Iris 程序逻辑验证使用效应处理器的 Wasm 程序。
初始化全局对象：时间与顺序
提出偏序与初始化时间无关性原则，用可模块化、可区域调优的静态分析保障全局对象安全初始化。
时间敏感的间歇计算遇上遗留软件
提出 TICS 平台，为间歇计算提供时间敏感编程抽象与可预测检查点，使遗留嵌入式代码无需重写即可间歇运行。
探索 C 语义与指针来源（pointer provenance）
提出两种 C 指针来源语义方案，将其实现为可执行测试预言，并结合 CHERI 移植与 SPEC 插桩评估。
Doo bee doo bee doo
提出严格函数式语言 Frank，用双向效果类型系统与推广的函数抽象统一 effect handlers，并引入 adaptor 支持效果封装与重连。
Qunity：一个统一量子与经典计算的语言
提出统一量子与经典计算的语言 Qunity，以统一语法和指称语义保证量子有效性，并可编译到 OpenQASM。
Enclosure：基于语言的不可信库限制
提出 Enclosure，用语言机制限制不可信库，防止公共库引入未审查代码带来的安全风险。
理解开发者对弃用作为语言特性的需求
通过访谈与问卷揭示 Java API 开发者对弃用机制的需求，并提出三项增强方案。
类型与作用域安全的带绑定语法宇宙：其语义与证明
提出一个类型与作用域安全的带绑定语法宇宙，可泛型实现遍历并泛型证明其性质。
用模态内存管理“氧化”OCaml
以 affinity、uniqueness、locality 三条 mode 轴实现可完全推断、向后兼容的 OCaml 栈分配与原地更新，安全减少堆分配。
Solidity 智能合约中的内联汇编研究
对以太坊 680 万份 Solidity 智能合约进行大规模实证研究，揭示内联汇编的使用率、演变与模式。
更快还是更慢？用经验证据揭开 Python 惯用法的性能谜团
通过大规模合成与真实项目数据，系统测量并字节码级解释 Python 惯用法相对非惯用写法的性能差异。
捕获类型
提出在类型中紧凑记录值所捕获自由变量的演算 CC<:□，并用于安全实现作用域能力与效应多态。
Whip：面向现代服务的高阶契约
提出 Whip 高阶契约系统，用面向服务的高阶契约语言和本地运行时监控，检测服务是否遵守声明的接口。
测试正则表达式的可推广性及其启示：一项大规模多语言测量研究
通过八项指标和53万余条正则的多语言测量，发现提取方法影响小但语言间正则特征差异显著，警示实证结论可推广性。
渐进依赖类型的近似规范化
提出 GDTL，以近似但全的编译期规范化支持渐进依赖类型，并证明类型检查可判定及渐进保证。
理解真实世界中的 Solidity 事件日志实践
首个基于 2,915 个 GitHub Solidity 项目的事件日志实践实证研究，并实现检查器发现高 gas 日志问题。
unsafe 是阿喀琉斯之踵吗？Rust 不安全编程中安全需求的全面研究
对 Rust 标准库 unsafe API 文档中的安全需求进行系统研究，揭示其不一致与不足，并建议统一规范。
MacoCaml：分阶段的可组合与可编译宏
提出 MacoCaml，一种结合宏、阶段分离和基于引用的 staging 的 OCaml 编译时代码生成设计，并给出形式化与实现。
基于代数效应的通用事件关联
基于代数效应与处理器，首次统一表达异步事件流上的多种 n 路 join 变体。
Ornaments 的本质
用多类签名抽象索引数据类型，为 ornaments 建立去语法化模型，使其可推广到 GADTs/refinement types。
Agda 中的交互式编程——对象与图形用户界面
提出 Agda 中基于共归纳 IO 与 copattern 匹配的交互式对象编程方法，实现 ooAgda 库并支持 GUI 与对象验证。
Verse 演算：确定性函数式逻辑编程的核心演算
提出 Verse 演算（VC），为确定性函数式逻辑编程提供小步重写语义，并证明良行为项的重写系统合流。
C++ 中的高层效应处理器
提出 cpp-effects 库，在带手动内存管理的 C++ 中实现带类型的高层效应处理器，并验证其性能竞争力。
Sparcl：一种部分可逆计算语言
提出线性类型语言 Sparcl，以部分可逆为常态，构造性保证程序可逆性并将双射作为特例。
Resilient X10 中的故障恢复
将 Resilient X10 从故障感知推进到故障恢复，把冗余与恢复负担转移给运行时与标准库，降低程序员负担。
选择性应用函子
提出选择性应用函子，介于应用函子与单子之间，可静态声明效果并动态选择执行。
有你或没你：使用效应排除进行编程
提出支持效应排他的类型与效应系统，可直接表达“除指定效应外皆可”的函数，并在 Flix 中实现。
1ML —— 核心与模块的统一
提出 1ML，将 ML 核心与模块统一为一种语言，使模块成为一等值，并用 System Fω 表达其类型结构。
特快专递：基于邮箱类型的编程
提出首个融入邮箱类型的编程语言 Pat，并用算法化类型系统静态防范 actor 通信协议错误与死锁。
面向语言特性的性能剖析
提出特性特定剖析，按语言构造报告性能开销，帮助程序员定位特定语言特性的昂贵使用。
增量式关系透镜
提出增量式关系透镜及变更传播语义，并实现语言级可更新视图，实验显示比非增量方案快数个数量级。
内联测试
提出内联测试，使开发者可在语句附近就地编写测试，并实现首个支持 Python 和 Java 的 I-Test 框架。
验证对象构造
针对面向对象语言中多构造器与设计模式带来的对象构造问题，研究对象构造的验证。
为野兽系上领结：F⋈ 中的重载、eta 展开与可扩展数据类型
提出 F⋈ 核心语言，用对偶不相交关系驯服 merge，使 union、intersection 和重载共存且类型安全、确定。
flap：一种融合词法分析的确定性解析器
提出确定性 Greibach 范式，将词法与语法分析融合，实现无 token 流的高效确定性解析器组合子库 flap。
Kindly Bent to Free Us：以 kind 弯折解放我们
提出 ML 扩展 Affe，以 kind 和约束类型实现线性/仿射资源管理与借用，且无需表达式内线性注解并保留完整主类型推断。
COCHIS：稳定且连贯的隐式机制
提出 COCHIS 演算，在保持类型安全、连贯性与类型替换稳定性的同时支持多态、局部作用域、重叠实例与高阶规则。
依赖类型的泛型零开销复用
在 Curry 风格依赖类型论中用恒等函数内部化泛型复用，使非索引与索引数据类型及其程序零开销复用。
多参与方会话 Actor
将多参与方会话类型引入 Actor 模型，通过角色与协议邮箱在 Python 中实现运行时通信安全验证。
Hefty 代数：高阶代数效应的模块化精化
提出 Hefty 代数，将高阶操作的展开过程模块化，从而在不改接口、不重编译的情况下支持高阶代数效应的实现与精化。
双向面向对象编程：迈向对象的程序化与直接操纵
提出首个支持对象程序化与直接操纵的双向面向对象语言，并实现 BiOOP 工具。
使用 match types 的类型级编程
提出 match types——类型级的模式匹配，在基于 System F<: 的演算中形式化并证明可靠性，并在 Scala 3 编译器中实现。
存在危机已解决：一等存在类型的类型推断
提出双向类型推断算法，在 Haskell 中无需项标注即可推断存在类型的引入与消除，并采用强存在类型。
作为宏的依赖类型系统
提出 Turnstile+：用宏实现依赖类型系统的高层元 DSL，支持快速原型化依赖类型语言与证明助手扩展。
通过语法糖推断作用域
提出作用域推断，将核心语言的作用域规则提升到表面语言，并证明脱糖保持 α-等价。
不受束缚的 Visitors
提出 OCaml 的 Visitors 类型导向生成器与 alphaLib 库，使含名字绑定的 AST 遍历与变换可组合、可定制且模块化。
揭示 Rust 生态系统中编译器不稳定特性的使用与影响
系统分析 Rust 编译器不稳定特性的使用与生态影响，并构建编译失败恢复工具。
关联效应：面向效应式编程的灵活抽象
提出关联效应，使类型类能抽象其函数签名中的效应、由各实例指定具体效应，并在 Flix 中实现。
可编译、可扩展的多语言 DSL（函数式珍珠）
提出 Racket 的 syntax-spec 元语言，使 DSL 实现兼得自动宏扩展与编译优化，并重新实现 miniKanren。
互递归的 iso 递归子类型
提出带声明子类型的 iso 递归类型核心演算，无需平方级膨胀即可表达互递归与高阶/混合种类子类型，并给出可高效检查的片段。
Haskell 中的高阶类型级编程
为 GHC 引入不可匹配箭头，支持类型族部分应用，并证明其可靠性。
归责转移有效吗？
提出经验方法评估契约系统中归责信息能否系统定位缺陷，并用其分析 Racket 契约系统。
泛型遍历的泛型派生
提出结合 lens 与 traversal 的泛型派生库，可自动生成高效的数据结构查询与修改遍历。
Python 代码中主导编程范式的探索性研究
提出自动化范式分类技术，并对十万余个开源 Python 项目进行分析，发现面向对象范式占据主导。
局部无名集合
用范畴论与名义技术为局部无名语法表示建立等式公理与初始代数语义，并证明其范畴等价于有限支撑 M-集拓扑斯。
线性限定类型：能力与唯一性的通用推断
提出线性约束，把隐式线性参数作为限定类型，扩展 GHC 约束求解器自动推断，降低 Linear Haskell 使用负担。
效应换效率：一等控制带来渐近加速
证明效应处理器能为 generic count 带来渐近运行时加速，且该优势无法由可变状态弥补。
将直接操作融合进函数式程序
提出基于操作的框架与 delta 语言 DM，将开发者对输出的直接操作自动融合进函数式源代码，实现代码不敏感的直接操作。
制造类型差异：交集类型上的减法作为广义记录操作
提出基于子类型与不相交关系的通用类型差运算，将记录上的删除/更新操作推广到函数与交集类型。
Rhombus：无需满屏括号的宏新方案
提出 Rhombus：在 Racket 上用中缀语法实现 Lisp 式宏与语言扩展的多绑定空间方案。
超越记号：定理证明语言的卫生宏展开
提出面向交互式定理证明器的卫生宏系统，同时解决意外名称捕获与语法扩展能力不足，并集成到 Lean 4。
共享与变异的余效应
提出用余效应跟踪命令式程序中的变量共享，并扩展类型系统以简洁建模唯一性与不可变性。
带方差的参数多态对称多重分派
首次形式化支持对称多重分派、多重继承和带方差参数多态的对象语言，并证明其类型可靠性。
在 ML 模块中用 Zipper 避免签名规避
提出 ZipML，以浮动字段和签名 zipper 消除 ML 模块的签名规避问题，并证明类型系统可靠。
带模块函子的分阶段编译
将多阶段编程与 OCaml 模块函子结合，形式化设计并证明类型可靠性与阶段区分。
终极条件语法
提出一种支持并行/嵌套匹配与条件模式流动的新型模式匹配语法，可脱糖到无回溯核心并保持语义。
相干微分 PCF
提出确定性微分 lambda 演算，基于非加性范畴语义，将 PCF 扩展为完全确定性的微分语言。
契约透镜：通过计算推理双向程序
提出带谓词契约的 contract lens 与双向计算律，用程序演算从规约推导高效双向变换。
同步迭代多个集合
提出 Synchrony 迭代抽象，使多有序集合的同步迭代和通用数据库连接可用推导式表达。
为 DOT 辩护：具有模式匹配和 GADT 风格推理的对象的理论基础
提出 cDOT 演算，为对象语言中的子类型重建提供形式基础，并将 GADT 风格推理编码进来。
Sparcl：一种用于部分可逆计算的语言
提出线性类型语言 Sparcl，以部分可逆为常态，在构造上保证程序可逆性并提升表达力。
用 Datalog 进行面向对象定点编程
设计 OODL 语言，将对象、动态分派和受控可变性融入 Datalog 式定点语义，并编译到 Datalog。
Taype：一种策略无关的不经意计算语言
提出Taype语言，将安全策略与程序逻辑解耦，并首次实现不经意代数数据类型与磁带语义。
引入与消去，左与右
提出四类引入/消去（左/右）规则构成的编程语言设计空间，并用双表达性原则与证明/反驳对偶分析其模块化影响。
领域特定语言的组合式嵌入
提出组合式嵌入，在 CP 语言中兼得浅层与深层嵌入优势，支持 DSL 语言复用、模式匹配与可扩展解释。
对象图编程
提出对象图编程 OGO，用 Cypher 声明式查询直接读写整个对象堆，并为 Java 实现两种原型。
关系机器演算
提出关系机器演算 RMC：一阶关系编程的基础模型，以语法对合与 Frobenius 幺半群字符串图统一多种计算模型。
处理作用域检查：动态作用域外泄检查的比较框架
首次形式化研究动态作用域外泄检查，提出并验证 Cause-for-Concern 检查，并与静态环境分类器比较表达力。
Hayroll：将 C 宏与条件编译翻译为 Rust 的模块化包装器
Hayroll 以模块化包装器方式让 C-to-Rust 翻译具备预处理器感知能力，恢复条件编译的可配置性与宏抽象，且不修改底层翻译器。
面向并发安全的动态区域所有权
提出动态区域所有权模型，为动态类型语言提供可解释的并发安全所有权检查。
前缀下的主类型推断：重新审视静态重载
提出 HMQ，将 HM 类型规则重构为“前缀下的类型推断”，直接推出与 Algorithm W 一致的主类型，并简化 FreezeML、HMF 及 Koka 静态重载的形式化。
零开销的词法作用域效应处理器
提出类型制导翻译，使词法作用域效应处理器在无效应时不增加主代码运行时开销，并形式化证明其正确性。
通过效应处理器实现的渐近加速
证明通用效应处理器使 generic count 获得渐近加速，差距源于单次与多次限定控制之别。
共享状态 actor 的编程与推理
提出 facet 记法，为可受控共享状态的 actor 语言提供理论、类型系统与行为类型系统，并报告实现经验。
未装箱数据构造器：或者，cpp 如何判定停机问题
为 ML 系语言提出可选择性未装箱数据构造器，并给出拒绝表示混淆的静态分析与终止性判定算法。
以透明性完善 OCaml 模块
提出 Mω 类型系统，覆盖 OCaml 模块中的 applicative/generative functor 与透明归属，并经 Fω 精化证明其可靠性。
布局敏感文法中的自动歧义检测
提出布局敏感文法的有界歧义检测方法，以SMT编码局部歧义并机器化验证，可找出最短歧义句。
安全对象初始化的概念框架：Celsius 模型的原则化与机器化可靠性证明
提出安全对象初始化的四条核心原则，并以最小演算 Celsius 及 Coq 机器化证明实现兼具表达力与简洁性的初始化系统。
Veracity：利用可交换性的声明式多核编程
提出声明式多核编程范式，程序员以顺序方式书写并显式标注代码片段的可交换条件，编译器据此自动并行化。
Chocola：统一 futures、transactions 与 actors 的并发语言
提出统一 futures、transactions 与 actors 的并发语言 Chocola，形式化语义并证明其保证。
数据类型声明的 kind 推断
系统研究数据类型声明的 kind 推断，为 Haskell98 与 PolyKinds 给出声明式及算法化规范并证明其性质。
对称 data 与 codata 的分解多样性
提出支持 data/codata 对称分解并可自动互译的语言，给出机器化验证与 IDE 实现。
ML 的全向类型推断：无论如何保持主类型性
提出全向类型推断，通过可挂起约束与增量实例化在 let-泛化下恢复 ML 扩展的主类型性。
打破强封装：Java 模块滥用的一项综合研究
首个针对 Java 模块系统强封装被破坏（BSE）问题的实证研究，基于 4,079 个 GitHub issue 刻画其症状、来源与解决方式。
数据驱动的基于证据的语法糖设计
通过挖掘 1.66 亿 Java 方法的频繁控制流子图，数据驱动地发现可新增语法糖以简化常见代码惯用法。
无运行时开销的安全底层代码是可行的
通过类型不变式证明潜在不安全操作的安全性，实证表明 Rust、C# 与 Ada 可无运行时开销实现安全网络设备驱动。
相对单子元语言
将单子元语言推广到相对单子设置，给出完备语义，并据此重新刻画 graded monads 与 arrows 并设计保守扩展语言。
Boolean-kinded 类型系统中的 let 泛化、多态递归与变量最小化
为 Boolean-kinded Hindley-Milner 扩展给出等式泛化与半统一算法，支持 let 泛化和多态递归，并最小化布尔类型变量。
将经典相继式演算编译到常规硬件：编译的对偶性
提出基于经典相继式演算的中间表示，并展示其可直接翻译到常规硬件，给出了形式描述、实现与初步性能评估。
面向动态语言的多态记录
为带集合论类型（并、交、否定）的记录引入行多态，给出子类型判定与类型检查算法，并证明类型系统可靠。
一阶惰性
提出一阶惰性构造子，将惰性数据结构中的 thunk 去功能化，从而提升性能并便于调试。
软件规约教学（经验报告）
报告以软件规约为中心的一年级课程经验，创建支持契约与性质测试的教学语言，并用学生访谈评估效果。
为 Rust 实现垃圾回收：终结器前沿
提出并实现 Rust 的 GC 方案 Alloy，首次让既有析构函数自动充当 GC 终结器，并解决由此带来的健全性与性能问题。
带效应的软件契约
在效应处理器语境下提出通用效应契约系统，并证明契约不会不当干扰程序执行。
递归结构化 Actor 契约中对接收者属性的 blame 正确支持
为 Actor 语言提出两种递归结构的新型契约，用于约束消息接收者及其通信行为，并证明 blame 分配的正确性。
静态可消解歧义
提出首个高效、实用且经 Coq 证明正确的静态可消解歧义方案，并集成到 OCaml 解析器。
依赖（余）模式匹配的加工：不遗漏任何模式
提出将依赖（余）模式匹配定义加工为核心语言 case tree 的算法，证明其保持首匹配语义并改进 Agda 实现。
部分类型构造子：或，让特设数据类型不那么特设
提出部分类型构造子的语言设计与形式理论，用限定类型刻画其定义域，支持部分数据类型作为一等公民。
使用高阶逻辑编程原型化函数式语言：一篇关于学习 λProlog/Makam 的函数式珍珠
展示如何用 λProlog/Makam 的高阶逻辑编程快速原型化带复杂类型系统的函数式语言实现。
迈向晚绑定面向对象系统的简洁绑定语义
用 Id 对象模型统一刻画 Smalltalk 与 Self 的方法绑定语义，并将二者视为不同特例。
Granthi：基于酉线路连线的高阶量子编程
提出纯酉高阶量子语言 Granthi，让量子程序成为可传递、相干复合的一等值并编译为静态量子电路。
面向可扩展变体与深层模式匹配的 trait 模块化类型安全
提出支持可扩展变体、深层模式匹配、方法重写、穷尽性保证与独立类型检查的 trait 语言，实现模块化类型安全。
演化趋势、使用模式与隐藏陷阱：揭示真实世界中的 JavaScript 语言特性使用
大规模实证分析 12 个 JavaScript/TypeScript 可替代特性的演化趋势、使用模式与代码坏味。
从模块到市场：跨组织可组合能力共享的愿景
提出跨组织能力市场愿景，以契约化、可部署模块实现高层软件能力的共享、发现与组合。
Token Sugar：用 token 高效简写让源代码对 LLM 更「甜」
提出 Token Sugar：将高频冗长代码模式替换为可逆简写，降低 LLM 代码任务的 token 开销并保持性能。
Actor 契约系统的软验证
为分布式 actor 程序提出契约语言并发展软验证技术，以在降低运行时契约检查开销的同时保留契约保障。
Clang __usercall：迈向对用户定义调用约定的原生支持
在 Clang 中实现 __usercall 属性，使 C/C++ 源码能以熟悉语法直接声明用户自定义调用约定，简化逆向工程中的函数对接。
面向实验的计算：一个倡议
提出将实验活动视为一类独立计算，并抽象实验特征，形成与软件工程问题正交的面向实验计算（EOC）方法。
AuDaLa 的表达能力：图灵完备性与可能的扩展
通过在 AuDaLa 中实现并验证图灵机，证明其图灵完备，并探讨提升实用表达力的扩展。
支持特设多态的可扩展数据类型
提出结合行类型/行多态与类型类特设多态的可扩展数据类型语言设计，并给出机器化验证的可靠性证明。
通过提升定位语法糖的类型错误
提出 Stellar 框架，通过提升核心语言类型规则，在表层语法中精确定位并报告可修复的语法糖类型错误。
基于示例与树自动机的文法修复
提出基于示例和树自动机的 CFG 歧义修复方法，可自动生成符合设计者意图且适合解析器生成的文法。
类型安全的单调对象演化
提出语言 May，用继承式单调对象演化与仿射权限系统，在允许别名时静态保证对象重分类安全。
函数式与命令式动态语言的类型推断
为同时支持函数式与命令式范式的动态语言提出基于集合论类型的类型系统与推断方法。
通过可撤销能力（Capabilities）实现 Typestate
将流不敏感的 capability 机制扩展为流敏感，解耦能力生命周期与词法作用域，实现安全且表达力强的 typestate 编程。
带有静态重载的句法隐式参数
提出句法隐式参数与静态重载两个正交机制，以简单实现覆盖隐式参数的常见用法。
C++ 函数模板的快速约束合成
提出基于轻量级过程间静态分析的 C++ 函数模板约束自动合成方法，可快速生成非平凡约束并缩短编译错误信息。
奇点积分与微分的语义
首次为支持奇点积分求值与微分的可微编程语言 SingularFlow 建立指称语义，并证明 Monte Carlo 操作语义是良态估计器。
轻量级且局部性感知的黑盒子程序组合
提出 Fern，通过轻量级声明暴露数据依赖模式，在保持模块性的同时融合黑盒子程序，最高加速 5 倍。
初始语义的 2-函子性及其应用
证明以 monoidal 范畴为参数的初始语义具有 2-范畴结构，并据此关联不同变量绑定表示下的模型。
基于布尔代数的限定类型
提出基于布尔代数的类型限定符，扩展 System F<: 并奠定 Flix 效果系统的形式基础。
面向效应处理器的 Dynamic Wind
为词法效应处理器设计并形式化了一种 dynamic wind，在任意控制效应下保持良定义语义与资源括约。
带物化义务的语法补全
提出 tall tylr：用可物化的语法义务抽象多种补全可能，并以 tile 解析演算保证任意输入都能恢复为良构项。
为一等环境辩护
提出基于环境的小步语义 λE，避免替换，自然支持一等环境并具 Coq 形式化。
读/写可因子化程序
通过类型系统区分只可析构与只可构造的数据，提出 RW-可因子化程序，将 cons-free 范式扩展到函数复杂度类。
Prisma：一种用于在去中心化应用中强制合约-客户端协议的无层语言
提出无层语言 Prisma，将合约与客户端统一编写，用 direct-style 通信原语保证接口协议一致。
Ghostbuster：简化并转换 GADT 的工具
提出 Ghostbuster，可省略选定类型参数来生成简化 GADT，并自动生成类型安全的往返转换函数。
Espresso：为 Java 及其运行时提供非易失性内存持久化支持
提出 Espresso，对 Java 与 JVM 做整体扩展，以高性能利用 NVM 实现持久化内存管理。
分阶段泛型编程
用多阶段编程将 Scrap Your Boilerplate 改造成带类型的优化代码生成器，消除泛型编程的性能开销。
Lineal：一种线性代数 Lambda 演算
提出扩展 Lambda 演算的线性代数演算 Lineal，允许任意线性组合项，给出重写规则并证明合流。
与特性交互共存（主题演讲）
探讨特性导向软件开发中特性并非独立关注点、会以意外方式相互干扰的问题。
抽象化代数效应
提出 λ_HEL 演算及存在/局部代数效应，用类型化运行时强制转换保障效应抽象不被破坏。
抽象可扩展数据类型：或，行类型无论何名
提出 row theories 与 qualified types，统一抽象可扩展记录和变体，并保持 coherence 与主类型。
Mœbius：使用上下文类型的元编程——System F 能对自身进行模式匹配的阶段
提出 Mœbius 元编程语言基础，支持多态代码生成与对开放代码的模式匹配，并证明类型保持。
组合式编程（Compositional Programming）
提出静态类型的组合式编程风格与 CP 语言，用组合式接口、trait、方法模式等概念同时解决表达式问题与模块化依赖。
违抗组件的谨慎自适应
提出一种谨慎自适应方法，通过面向切面包装器在异常条件下改变违抗组件行为，同时保证其个体需求与系统全局需求。
Choral：面向对象的编排编程
提出首个面向对象编排编程语言 Choral，将编排编译为各角色的纯 Java 库以实现模块化分布式开发。
带类型类的分阶段编程：类型化 Template Haskell 的一个规范
提出 staged type class constraints，形式化为源演算 λ⇒ 与核心演算 F，证明类型健全性，解决代码引用与类型类的不健全交互。