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
标签：类型系统（共 794 篇，按优先级展示前 200）
Numerical Fuzz：一种面向舍入误差分析的类型系统
提出带线性灵敏度与分级单子的类型系统 Λ_num，静态推导浮点舍入误差的定量界并证明其语义可靠性。
神经符号模块化精化类型推断
提出神经符号 agent LHC，用 LLM 自动生成整包精化类型标注并由 LiquidHaskell 验证，大幅降低形式验证标注成本。
Refty：基于细化类型的深度学习模型静态检查
提出基于细化类型的工具 Refty，用 SMT 求解算子约束，在运行前静态检测深度学习模型的类型错误。
Bean：一种用于后向误差分析的语言
提出 Bean 语言及带分级 coeffect 与严格线性的类型系统，静态推导浮点程序后向误差界，并用范畴语义证明可靠性。
通过类型系统刻画条件独立性
提出信息流类型系统捕获概率模型的条件独立性，并用类型推断与程序变换自动消除离散参数。
使用语言模型的类型约束代码生成
提出类型约束解码：用前缀自动机与可居留类型搜索保证 LLM 生成代码良类型，编译错误减少过半。
面向代码优化的具体类型推断：结合机器学习与 SMT 求解
提出结合机器学习与 SMT 求解的具体类型推断，无需类型标注即可优化动态类型 Python 代码。
可编程 MCMC 与可靠组合的引导程序
提出基于协程和类型系统的框架，验证可编程 MCMC 中用户引导程序的正确性与可组合性。
用正则表达式跟踪借用
提出以正则表达式跟踪访问路径的借用检查类型系统，经 Lean 机械化并部署于 Sui 的 Move 字节码验证器。
RunbookFX：面向可执行事故诊断与缓解的类型与效应安全的 LLM 合成
提出类型化函数式 DSL RunbookFX，用乘积效应代数把事故响应安全分解为风险、能力、回滚三维，并以 Coq 机化证明保障 LLM 合成程序的安全性。
面向 Python 的生成式类型推断
提出 Typegen，将静态分析步骤转为思维链提示，实现少样本、可解释的 Python 类型推断。
Phys：概率化物理单位分配与不一致检测
提出概率推断方法，从变量名和表达式线索中分配物理单位并检测不一致，显著提升覆盖率和准确率。
面向同态加密的带 reserve 的性能感知尺度分析
提出性能感知的静态 scale 分析，通过 reserve 预算反向重分配，无需空间探索即可生成高效尺度管理方案。
基于信息流的概率程序编译与变量消除
提出一种编译方法，利用信息流类型系统分解概率计算，将递归概率程序的全局边缘推断化为可处理子问题。
自动化即时 Python 类型标注更新
提出基于 LLM 的 TypeUp，利用代码变更与旧标注即时更新 Python 类型标注，并显著优于 TypeGen。
NL2Type：从自然语言信息推断 JavaScript 函数类型
利用注释、函数名与参数名等自然语言信息，以 LSTM 预测 JavaScript 函数类型签名，并可用于检查类型注解一致性。
静态推断遇上深度学习
提出 Hityper，通过类型依赖图将静态推断规则与深度学习预测结合，迭代完成动态语言类型推断。
学习类型注解：大数据足够吗？
提出 TypeBert，用简单 token 序列归纳偏置与大规模数据，在 TypeScript 类型注解预测上超越复杂模型。
Fuzzi：一种面向差分隐私的三层逻辑
提出面向差分隐私的三层逻辑 Fuzzi，打通敏感度类型逻辑与 apRHL，实现自动且灵活的隐私验证。
你只需线性化一次：切向量转置成梯度
将反向模式自动微分分解为正向模式、线性/非线性解压与线性部分转置，并证明其正确性。
在 SlicStan 中基于密度的概率编程：高效、灵活且确定性
为 Stan 给出基于密度的操作语义，并设计可组合、自优化的 SlicStan，再保义翻译回 Stan。
可空性类型的实用推断
提出以类型检查器为黑盒 oracle 的可空性类型限定符自动推断方法，并实现 NullAwayAnnotator，平均减少 69.5% 的 NullAway 错误。
类型保持、依赖感知的 guide 生成：面向可靠且有效的摊销概率推断
用行为类型系统驱动类型导向翻译，自动生成概率程序的 guide，保证可靠性并提升摊销推断效果。
安全耦合：耦合式精化类型
受概率耦合启发扩展精化类型，在 Liquid Haskell 中验证概率计算的关系性质与机器学习实现。
QuAC：面向 Python 的快速属性中心类型推断
提出 QuAC，通过收集 Python 表达式访问的属性集合并用信息检索预测类，实现快速准确的类型推断。
TIGER：面向实用 Python 类型推断的“先生成后排序”框架
提出两阶段“先生成后排序”框架，显著提升 Python 中用户定义类型与未见类型的推断准确率。
热带数学与λ演算 II：概率编程语言的热带几何
将热带几何用于高阶概率程序的统计推断，并设计交集类型系统组合式估计最可能运行。
概率程序的类型导向离散化
提出类型导向的全局变换 Slice，将连续概率程序精确离散化，保持语义并赋能离散推断引擎。
TypeCare：通过上下文感知的重排序与数据增强提升 Python 类型推断模型
提出上下文感知重排序与数据增强方法 TypeCare，提升 Python 类型推断模型对稀有与复杂类型的推断能力。
用于验证 eBPF 程序的流敏感精化类型系统
提出流敏感精化类型系统，在用户态自动推断 eBPF 验证证明证书，缩小可信基并提升可调试性。
深度学习类型推断
提出 DeepTyper，用深度学习结合编译器为 JavaScript 等动态语言预测并补充类型标注，准确率高。
Type4Py：基于深度相似度学习的 Python 类型推断
提出 Type4Py，用深度相似度学习的层次神经网络在类型空间中聚类，为 Python 参数、变量与返回值推断类型。
通过静态信息流分析验证实用硬件安全架构
提出安全类型 HDL，通过静态信息流分析验证 ARM TrustZone 多核原型等硬件安全机制，并能发现漏洞。
提升期望：用类型自动进行期望成本分析
提出基于类型的概率程序期望执行成本上界分析，支持高阶函数与归纳数据类型，并将推断归约为线性约束求解。
概率语言中可靠可编程推断的迹类型与指称语义
提出迹类型系统与指称语义，使可编程推断程序在构造上保证可靠性，覆盖变分、SMC、MCMC 等。
基于度量的概率关系推理
扩展 Fuzz 以支持概率程序的一般关系性质，并用范畴语义刻画概率散度组合，覆盖近似差分隐私。
带线性否定的简单类型 λ-演算中的反向传播
将反向传播从一阶计算图扩展到带线性否定的简单类型 λ-演算，并保持一阶反向传播的效率。
CN：用分离逻辑精化类型验证系统 C 代码
设计并实现 CN——面向系统 C 代码的分离逻辑精化类型系统，并验证 pKVM 组件。
概率函数式程序的基于类型的复杂度分析
提出 λRPCF 类型系统，通过动态分布类型与 Lyapunov 秩函数，对概率高阶函数式程序进行组合式平均情形复杂度分析。
精确递归概率编程
提出一种概率编程语言，可自然表达递归数据上的递归，并通过类型保证的程序变换实现精确推断。
一种用于概率性不经意计算的语言
提出核心语言 Lambda Obliv，用子结构类型系统与「概率区域」静态保证概率程序的不经意性，并修复 ObliVM 的不健全性。
模式化数据竞争自由
扩展 OCaml 类型系统，以 mode 保证多线程数据竞争自由并兼容顺序代码。
TypeWriter：基于搜索验证的神经网络类型预测
将神经网络类型预测与搜索式验证结合，为动态语言自动补全正确类型注解。
Tree Borrows（树状借用）
用树结构替代栈定义 Rust 别名模型 Tree Borrows，更精确刻画 unsafe 代码行为，大幅减少误报并保留与新增编译器优化。
带正则递归类型的自动摊销资源分析
为任意正则递归类型定义的代数数据结构构造资源多项式，并在 AARA 资源类型系统中实现复杂数据结构上的自动资源界推断。
计算图抽象的几何
用动态交互几何为按值λ演算中的计算图抽象建立类型系统与语义模型，保证垃圾回收和β律安全。
基于依赖细化类型系统的高阶概率程序自动验证
提出依赖细化类型系统，将高阶概率程序的多种定量性质验证归约到扩展 CHC 求解，并可复用现有求解器。
高阶概率程序中期望代价的模态类型论
提出 pλ-amor，用分级模态类型论证明高阶概率程序的期望代价界。
SA4U：面向单位类型错误检测的实用静态分析
无需修改固件或开发者标注，通过分析仿真轨迹与协议定义推导变量单位类型，检测无人机固件中的单位类型错误。
并行计算图的静态预测
提出图类型（graph types），静态推断并行程序所有可能的计算图，并用于死锁检测与开销分析。
Java 与 Lambda：一个 Featherweight 故事
提出核心演算 FJ&λ，形式化 Java 8 的 lambda、交集类型与接口默认方法，并证明类型安全与推断。
泛型精化类型（Generic Refinement Types）
提出泛型精化类型，用 ghost 参数抽象函数契约不变量，保持 SMT 可判定验证并在 Rust 中实现。
FlexType：面向类型推断模型的即插即用框架
提出 FlexType——一个可插拔的 IDE 扩展，能在 JavaScript 与 TypeScript 中交互或自动推断类型。
NullAway：面向 Java 的实用型基于类型的空安全
提出 NullAway，一个构建开销低、注解负担小的 Java 空安全类型检查器，可在每次构建中运行。
函数式张量语言的已验证编译器
为函数式张量语言 ATL 的降级算法提供形式化正确性证明，并用新类型系统修复截断 reshape 的可靠性缺陷。
一种实用的递归定义模式系统
提出一种实用的模式系统，静态检测 call-by-value 递归定义中的恶性循环，并成功替换 OCaml 的不健全语法检查。
编译到线性神经元
提出类型化高阶线性语言 Cajal，并证明其程序可编译为线性神经元，从而以可微方式直接编程神经网络。
动态释放信息流策略的健全强制执行
提出首个健全强制执行动态释放信息流策略的类型系统，形式化证明其可靠性并实现 Rust 原型。
嵌套归纳类型：Lean 与 Rocq 中有依据且可用的嵌套归纳类型
提出嵌套归纳类型的有效性判据，保证可展开为互归纳类型，并自动生成正确的消去原理。
Verus：使用线性幽灵类型验证 Rust 程序
提出基于 SMT 的 Verus，用线性 ghost 类型与模式系统验证 Rust 程序的功能正确性。
基于行为类型的 Go 消息传递静态验证框架
提出基于行为类型的静态验证框架，用于检查 Go 通道消息传递程序的并发正确性。
Cubical Agda：一种支持 univalence 与高阶归纳类型的依赖类型编程语言
通过 cubical 原语扩展 Agda，使其原生支持 univalence 与高阶归纳类型并保持构造性。
RefinedRust：面向 Rust 程序高保障验证的类型系统
提出在 Coq 中证明可靠的精化类型系统，支持 safe 与 unsafe Rust 代码的基础性半自动功能正确性验证。
Obsidian：面向智能合约的安全编程语言
提出 Obsidian 语言及其核心演算 Silica，用 typestate 与线性类型静态检测智能合约常见漏洞，并证明类型可靠性。
使用 Idris 进行类型驱动开发
介绍 Idris 中依赖类型驱动的开发方法，面向工程师，涵盖函数式编程、依赖类型与程序验证。
Blade：自动消除密码代码中的推测性泄漏
提出 Blade，用类型系统与 protect 原语自动切断推测性秘密的数据流，消除密码代码中的推测泄漏。
异常异步会话类型：无需层级（tiers）的会话类型
首次将异步会话类型与异常处理集成到函数式语言，给出核心演算与 Links 实现。
切入要点：pointful 数组编程的索引集与保持并行的自动微分
提出将数组视为类型化索引集上的函数，并用类型化效应支持可自动并行化原地更新及保持并行的反向自动微分。
Liquidate your assets：在 Liquid Haskell 中推理资源使用
展示如何用 Liquid Haskell 的 refinement types 在同一框架中验证程序效率与资源使用。
基于时间会话类型的并行复杂度分析
提出时间会话类型，将线性逻辑会话类型扩展以局部、组合地分析并发消息传递程序的参数化并行复杂度。
面向复杂度分析的自动化 sized 类型推断
提出一种基于 sized 类型推断、ticking 单子变换与约束求解的全自动高阶函数式程序复杂度分析方法。
Quick Look：非直谓类型推断
提出 Quick Look 设计，在 GHC 中实现非直谓类型推断，使多态类型成为一等公民，且改动局部且兼容现有扩展。
Flux：面向 Rust 的液体类型
提出 Flux，将逻辑精化与 Rust 所有权结合，实现指针程序的易用类型验证与液态推断。
MLstruct：结构类型布尔代数中的主类型推断
提出 MLstruct，在结构记录、等递归类型与一阶并/交类型下实现主多态类型推断。
RefiNym：利用名称精化类型
提出 RefiNym，通过名称流无监督挖掘概念类型并具体化为名义类型，以精化程序类型。
用于时序性质验证的不动点逻辑与依赖效应
提出依赖精化类型与效应系统及不动点逻辑演绎方法，以组合化验证高阶函数式程序的时序性质。
Liquid 信息流控制
提出 Lifty，用 liquid types 静态验证敏感数据信息流策略，并自动合成修复补丁。
底层沙箱化的高层收益
证明沙箱化可使受信任代码在任意不可信代码存在时仍保持类型安全（鲁棒安全），并在Coq中机械化验证。
一个成本感知的逻辑框架
提出 calf 成本感知逻辑框架，以依赖类型论统一程序行为与成本推理，并在 Agda 中机器化验证算法复杂度。
驯服重写：一种带计算假设的类型论
提出重写类型论 RTT，允许把计算假设写成重写规则并自动用于类型检查，同时保持类型可靠性。
基于单子仿射大小类型的概率终止
提出单子仿射大小类型系统，可类型化概率高阶程序并证明其几乎必然终止。
局部精化类型化
提出 FUSION 算法实现局部精化类型推断，用 SMT 验证多态数据类型与高阶函数，显著减少模板并加速。
Multiparty GV：具有经认证无死锁性的函数式多参与方会话类型
提出函数式多参与方会话类型语言MPGV，支持一等端点并保持无死锁性，结果已在Coq中机器验证。
交集类型与（正）几乎必然终止
用非幂等交集类型同时刻画随机λ演算的收敛概率与正几乎必然终止，并证明其可靠完备且递归论最优。
面向摊还分析的指称式递推提取
将递推提取扩展到摊还分析，引入带信用标注的仿射中间语言，并证明其到递推语言的指称正确性。
利用 Rust 类型进行程序合成
提出首个面向安全 Rust 的按构造正确程序合成方法，用 Synthetic Ownership Logic 将类型约束与功能规约结合。
一个合理异常的类型论
提出三层 RETT，在完全依赖类型论中首次一致地推理异常项，并提供 Coq 插件 CoqRETT。
面向可用性的 Java Liquid Types 设计
以参与式设计将 Liquid Types 融入 Java，实现 LiquidJava，并经 30 人用户研究证明其易学易用且能帮助发现并修复更多缺陷。
CRDT 收敛性的类型检查
提出 Propel 语言与类型系统，用类型检查自动验证 CRDT 实现所需的交换、结合、幂等等代数性质。
用于灵活内存管理的引用能力
提出基于引用能力的属主类型系统，强制 Verona 中区域隔离，支持对象跨区域与线程移动，且数据访问无需原子操作。
依赖类型的数据平面编程
提出基于可判定精化的依赖类型 P4 方言 Π4，为数据平面程序提供轻量级静态验证。
类型指导的自然语言查询到可视化合成
将自然语言查询转为 refinement 类型规约，并用类型指导合成生成符合用户意图与设计准则的可视化程序。
数据流精化类型推断
提出参数化精化类型系统，用抽象解释刻画数据流语义并导出推断算法，统一并推广现有方法。
Curry 与 Howard 遇上 Borel
建立计数命题逻辑与概率事件 λ 演算的 Curry-Howard 对应，并以交集类型精确刻画概率行为。
基于洞的完全类型错误定位与恢复
提出标记 lambda 演算，首次形式化完全类型错误定位与恢复，并在 Hazel 中实现无无意义编辑器状态的实时环境。
带宇宙与擦除的分级模态依赖类型理论及其形式化
提出带宇宙与擦除的分级模态依赖类型理论，并在 Agda 中形式化，证明元理论性质与擦除提取的可靠性。
Liquid 资源类型
提出 Liquid 资源类型，用精化类型与潜势标注自动验证函数式程序的精确资源消耗界。
类型引导的最坏情况输入生成
提出基于 AARA 类型推导的最坏情况输入生成方法，可证明资源界紧致并生成大规模测试输入。
量子电路描述语言中灵活的基于类型的资源估计
为 Quipper 设计基于效应与细化类型的类型系统，自动推导电路宽度、深度、门数等资源上界。
面向非纯高阶语言的图中间表示：以精确效应依赖实现可负担的激进优化
提出结合可达性类型与效应系统的类型化图IR，为含副作用与高阶函数的语言提供精确依赖与廉价激进优化。
论类型分支、联合消除与出现类型（occurrence typing）
扩展联合/交集类型系统加入 type-case，证明其与联合消除可涵盖 occurrence typing，并给出类型重建算法。
命题即类型与共享状态
将共享可变状态融入会话并发语言的命题即类型线性逻辑解释，并保持安全与活性。
从参数性导出简单的非干扰性
利用参数性在构造演算中证明 polyvariant DCC 的非干扰性，并给出 Agda 机械化证明。
Futhark 中高阶模块的静态解释：面向大规模的函数式 GPU 编程
为纯函数式数据并行语言 Futhark 设计高阶模块系统，并在 Coq 中形式化其静态语义与编译期消除。
调和非干涉与渐进类型
研究如何调和信息流控制中的非干涉与渐进类型，以恢复动态渐进保证。
LLF_𝒫：一个使用 monad 建模外部证据、边条件与证明无关性的逻辑框架
扩展 LF 提出 Lax Logical Framework LLF_𝒫，用 Lock monad 表达边条件、外部证据与证明无关性，并证明其保守性。
面向 CIC 的新合一器可理解指南：包含宇宙多态与重载
完整描述并实现支持宇宙多态与重载（规范结构）的 CIC 合一算法，并在大型库上验证启发式足够。
Decalf：一个有向、带效应且成本感知的逻辑框架
提出 Decalf，用内在前序刻画带效应函数式程序成本界的有向成本感知逻辑框架，并给出单纯集模型。
概率资源感知会话类型
提出概率会话类型与嵌套多重宇宙语义，实现自动期望资源分析并开发 NomosPro 工具。
Kind 即调用约定
提出一种新的中间语言，将调用约定编码在类型的 Kind 中，从而兼顾灵活多态与高效静态编译。
证明相关的合一：仅使用你的类型论公理的依赖模式匹配
提出证明相关的合一框架，使合一规则只依赖所在类型论自身的公理，并据此重写 Agda 的合一算法修复大量缺陷。
面向大规模系统验证的线性类型
将线性类型与SMT验证结合并集成到Dafny，可显著减少内存推理的证明量与验证时间。
时间化会话类型
提出时间化会话类型，给出判定合规性与构造最精确合规对端（及子类型可判定性）的可靠完备技术。
Typestate 导向编程的化学方法
提出基于化学隐喻的 typestate 导向编程，以消息分子和化学反应建模并发状态变换，并用行为类型控制对象协议与共享。
D<: 的不可判定性及其可判定片段
证明 D<: 的类型检查与子类型不可判定，并给出两个可判定片段与判定算法。
面向智能合约中记账错误的发现
提出抽象类型传播与检查系统，将智能合约业务逻辑建模为银行式原语，以自动发现记账错误。
Python 静态类型推荐
提出静态类型推荐方法 Stray，为 Python 代码正确推荐类型注解，精度与召回率显著优于机器学习基线。
抽象函数即类型：依赖类型论中成本与行为的模块化验证
在单价依赖类型论中把抽象函数编码为类型，用相位区分与密封效应支持成本与行为的模块化验证。
生成非“无用”的良类型项
提出一种非局部生成算法，生成会使用参数的良类型函数，显著提升编译器随机测试效率。
GenSQL：一个用于查询数据库表生成模型的概率编程系统
在 SQL 上增加少量概率查询原语，构建可查询表格数据生成模型的概率编程系统 GenSQL，并给出类型系统、指称语义与可靠性证明。
一个 HAT 技巧：使用符号有限自动机自动验证表示不变式
提出 Hoare 自动机类型，将符号有限自动机融入精化类型，以自动验证依赖有状态库的数据结构表示不变式。
Call-by-Push-Value 中的效应与余效应
将效应与余效应追踪引入 CBPV 类型系统，证明其可靠性并在 Coq 中机器化验证。
C 语言的类型推断
提出基于合一的类型推断框架，恢复 C 程序中缺失的 struct、union、enum 与 typedef 声明，用于重建部分程序。
覆盖所有情况：测试输入生成器的基于类型验证
提出基于精化类型与 must 式欠近似推理的验证方法，确保测试输入生成器覆盖所有可接受输入。
依赖类型理论的可扩展相等性检查算法
提出一种用户可扩展的相等性检查算法，适用于一大类依赖类型理论，并在 Andromeda 2 中实现。
工业界的依赖类型 Haskell（经验报告）
报告在 GHC 中编码依赖类型编程的工业经验：可行且有价值，但成本高昂。
基于效应类型与线性依赖的电路宽度估计
提出 Proto-Quipper-R，用线性依赖类型与效应系统推导电路宽度参数上界，并实现 QuRA 工具验证。
有类型–无类型交互：比较分析
提出统一评估框架，对比若干主流有类型–无类型交互语义，帮助设计者分析自身动态语义的保证。
协变与逆变：对一个老问题的新审视（供函数式程序员学习的进阶类型系统入门）
重新审视面向对象方法参数的协变/逆变特化，论证二者可在同一语言中共存，并以实例讲解进阶类型系统概念与实现技巧。
纯同构类型系统（Pure Iso-Type Systems）
提出 PITS 演算族：以统一语法兼顾项与类型、支持无限制一般递归，并通过 iso-types 与显式 cast 保持类型检查可判定。
无需类型系统特定代码的可插拔类型推断
提出通用可插拔类型推断算法，复用局部推断，在 Checker Framework 实现，平均减少 45% 待注解警告。
支持内涵分析的元编程依赖类型理论
提出 DeLaM 分层模态依赖类型理论，支持开放代码的引用、组合、递归分析与类型安全代码生成。
基于类型驱动变异的 C++ 编译器模糊测试
提出首个面向 C++ 类型系统的变异式编译器模糊测试方法 TyMut，通过类型驱动变异与 must 分析发现 102 个编译器缺陷。
外延相等保持与已验证泛型编程
提出外延相等保持原则，在内涵类型论中无需扩展理论或完整 setoid 即可进行已验证泛型编程。
类型化与困惑：研究渐进类型（gradual typing）的意外危险
通过 3 万个开源仓库的实证研究，揭示渐进类型标注可能误导开发者、削弱运行时检查并引发类型混淆。
QuickSub：高效的同构递归子类型判定
提出高效易实现的同构递归子类型算法 QuickSub，最坏复杂度 O(nm)，常见情况近线性，并用 Coq 形式化验证。
无需区间的内部参数性
提出一种无需显式区间或高维立方语法的内部参数性类型论，并以预层与胶合模型证明外部参数性与 canonicity。
面向静态安全 WebAssembly 的索引类型
提出 Wasm-precheck，用索引类型静态检查程序值约束，从而安全移除 Wasm 的动态安全检查。
精化类型反驳
提出精化类型反驳，将双向类型检查规则系统化转为失败解释，支持全局精化推断，并实现于 Liquid Haskell 扩展 HayStack。
使用基于速率的会话类型验证 IoT 设备
提出带周期递归的定时进程演算与基于速率的会话类型，保证 IoT 消息传递的速率正确性，并在 Rust 中实现原型。
嵌套会话类型
为会话类型引入 prenex 多态与嵌套递归数据类型，证明类型等价可判定并提出高效可靠算法。
函数式-命令式环境下的关系成本分析
提出类型-效应系统 ARel，借助跟踪可变数组关系的类型精化，形式化推导函数式-命令式程序间的相对求值成本界。
参数化转换演算与可复用的渐进类型lambda演算元理论
提出两个参数化转换演算与可复用元理论，统一渐进类型lambda演算变体并在Agda中机械化。
将基于指针的优化封装在纯函数之后
利用依赖类型将指针地址操作封装为纯接口，使函数式程序保持引用透明并获得图级遍历性能。
资源感知会话类型的工作量分析
提出资源感知会话类型，静态推导消息传递并发进程的最坏情况总工作量。
面向定时消息传递协议的语义逻辑关系
提出完全语义的逻辑关系，用于验证异构应用与硬件设备对定时消息传递协议的合规性，并配以 refinement 类型系统与 Rust 类型检查器。
论简单类型 lambda 演算的可判定与不可判定扩展
给出 finitary PCF 四种扩展不可判定性的简单证明，并用类型系统刻画含引用单元的可判定片段。
实用类型推断中的层级（Levels）
首次系统形式化类型推断实现中广泛使用的 levels 技术，并说明其可用于实际类型推断实现。
非良类型程序不会求值
提出双侧类型系统，可反驳类型公式，从而保证良类型程序不出错、非良类型程序不会求值。
类型推断逻辑
提出一套逻辑框架，使约束式类型推断与elaboration能在Coq中模块化地机器验证其可靠性与完备性。
向 λμ-演算中添加否定
在 Parigot 的 λμ-演算中引入否定类型构造及语法构造，并证明其归约合流、强规范化与主类型性质。
渐进概率 lambda 演算
提出并形式化 GPLC，首个渐进类型的概率 lambda 演算，证明其类型安全并满足渐进保证。
内涵数据类型精化：应用于模式匹配安全性的可扩展验证
提出用于模式匹配安全验证的内涵数据类型精化类型系统，其推断可靠、完备且接近线性时间。
类型错误的系统性识别与传达
提出 counter-factual typing 与 variational typing，系统定位类型错误、生成纠错信息并排序呈现最可能原因。
通过子结构依赖追踪进行安全推理
提出基于输出约束的子结构类型框架，统一刻画能力、定量信息泄漏、沙箱与授权协议等安全特性，并以单一逻辑关系证明其安全性。
Trocq：超越等价与 univalence 的免费证明转移
提出 Trocq 证明转移框架，基于新的类型等价表述推广 univalent parametricity，并实现为 Coq 插件。
单态化的简单本质
提出基于类型流分析的简单单态化技术，可处理高阶与存在类型，并证明其类型与语义保持。
盒子里有什么：面向泛型数据结构的人机工程学与表达力兼备的捕获跟踪
提出 System Capless 与 reach capabilities，使捕获类型能跟踪泛型数据结构内的能力，并在 Scala 3 中实现与验证。
Cubical Agda 的内部参数性与观察式参数性
提出首个实用的内部参数性证明助手 Agda--bridges，并基于 SRP 给出内部自由定理的单行证明。
语义类型引导的缺陷发现
提出语义类型反驳器，借助符号求值证明函数式程序的语义类型性质不成立，从而发现类型错误。
面向底层代码内存静态分析的依赖名义物理类型系统
提出依赖名义物理类型系统，可嵌入抽象解释器，自动证明底层 C 与机器码的类型安全及空间内存安全。
区域推断上下文中的并行性
为基于区域推断的编译器设计 fork-join 并行构造，并给出类型规则、动态语义、类型可靠性及效应推断算法。
显式精化类型
提出 λert 类型理论，让程序员显式嵌入精化性质的证明，从而支持量词和归纳，并用 Lean 4 证明其可靠性。
概率高阶不动点逻辑（PHFL）
提出概率高阶不动点逻辑 PHFL，证明其表达力与模型检测的不可判定性，并用类型系统刻画可判定片段。
异构二叉随机访问列表
提出按类型索引的异构二叉随机访问列表，为依赖类型求值器提供支持随机访问的环境表示。
全有或全无：库类型注解如何影响 Python 客户端错误
研究 Python 库类型注解对客户端代码错误的影响，并提供完整可复现实验制品。
Scala 的一等精化类型
为 Scala 3 设计一等精化类型，使精化与子类型、推断、模式匹配统一整合，并机化证明核心演算的类型可靠性。
在立方类型论中自动化边界填充
提出面向立方类型论的边界填充自动化方法，统一求解 contortion 与 Kan 问题，并实现 Haskell 求解器。
一种基于补运算的错误性类型化方法
提出以正规形集合为类型语义、带补运算的双侧类型系统，可同时验证函数式程序的正确性与错误性。
用于局部敏感性分析的依赖余效应
提出 Local Fuzz：带依赖余效应的类型系统，刻画程序局部敏感性，给出优于 Fuzz 的差分隐私保证。
既要编码又要吃到蛋糕：在类型论中局部地控制计算
提出 LRTT 类型理论，以局部抽象封装用户自定义计算规则，并给出保守性证明与 Rocq 原型。
Let It Flow：异步数据流的形式化验证编译框架
首个对异步数据流编译器进行形式化验证的工作，用能力类型系统与 Lean 机器化证明同时保证确定性与流水线优化。
集合论类型在 Erlang 中的实践（经验报告）
将集合论类型检查器 Etylizer 应用于自身实现，实证其在真实 Erlang 代码中的表达力、可用性与可扩展性。
概率精化会话类型
提出概率精化会话类型 PReST，以符号化精化推理支持非常量概率的并发概率程序验证。
McTT：一个经过验证的证明助手内核
提出并实现 McTT，一个在 Rocq 中验证、可提取为 OCaml 的 Martin-Löf 类型论内核。
从线性到借用
逐步为线性类型演算加入不可变借用、词法生命周期、再借用与可变借用，并用分离逻辑证明其语义类型安全。
基于序维护的增量双向类型检查
提出用顺序维护数据结构实现增量双向类型检查，细粒度编辑后快速传播类型更新，性能较从头重分析快多个数量级。
ad hoc 解析器正则文法的静态推断
提出用精化类型推断从无标注 ad hoc 解析器源码中静态推断正则输入文法，并实现 Panini 系统。
结构化信息流：重新审视非干扰的类型
提出结构化信息流类型系统，基于混合逻辑自然地支持解分类，并通过逻辑关系证明非干扰性。
面向 GQL 的灵活且富有表达力的带类型路径模式
为 GQL 核心片段提出带不精确类型的类型系统 FPPC，静态检测空查询与卡住查询并保证类型安全。
RestPi：面向 REST API 的路径敏感类型推断
提出路径敏感类型推断引擎 RestPi，为 Ruby REST API 自动生成更精确完整的响应类型规约。
命令式组合式编程：经双向类型化实现带可变引用的类型安全分配性交集子类型
用双向类型化仅限制引用规则，在保留分配性交集子类型的同时为组合式编程加入可变引用，并机器化验证类型安全。
CoolerSpace：一种用于物理正确且计算高效的颜色编程语言
CoolerSpace 通过赋予物理量纲的类型系统与等式饱和优化，让颜色编程既物理正确又计算高效。
以参数性推导敏感度
提出用参数性从类型检查直接导出函数敏感度，并在 Haskell 库 Spar 中实现。
证明无关命题类型的无归约规范化
为含宇宙层级与证明无关命题的类型理论给出无归约规范化及转换可判定性证明，且无需显式中性与范式。
通配符需要见证保护
提出存在类型见证保护机制，形式化核心演算并证明可靠，可避免 Java 通配符不健全性且误报极少。
面向优化动态信息流控制的类型系统
提出流敏感类型系统 MinIF，静态消除动态 IFC 的运行时检查与标签跟踪开销，并保持程序行为与执行决策不变。
用效应系统对抗供应链攻击
提出效应安全的包升级与效应感知包管理器，借助效应锁文件阻止供应链攻击。
对能力进行分类（Classifying Capabilities）
提出树状、可扩展的 capability 分类器，按语义角色过滤捕获集并支持可判定的不相交推理，在 Scala 3 中实现并于 Lean 4 机器化验证。
使用可组合递归模式与变换进行编程
提出 CRPT：可组合递归模式与变换，将递归类型定义用于无回溯的线性时间识别与变换，并给出类型系统与实现。
高阶逻辑中的句法效应化可实现性
提出 EffHOL，将句法可实现性推广到带副作用的计算，并通过 monad 参数化抽取效应化实者。
类型自动机
提出类型自动机，以程序类型为控制与存储，连接类型系统与自动机理论并支持类型级元编程。
基于专用类型检查器的轻量级验证
利用可插拔的专用类型检查器降低验证门槛，以更易用的方式解决以往需复杂验证技术的问题。
验证顺序程序中的确定性
提出一种类型系统，在编译期可靠验证顺序程序的计算是确定、非确定还是序非确定的，并在大型程序中检出未知缺陷。
面向动态语言的类型化中间表示
提出类型化高层 IR，显式表达动态语言特性并支持特化、内联、作用域与拷贝消除等优化。
SQL 引擎中类型与类型转换语义的形式化框架
提出 TRAF：一种刻画 SQL 静态与动态类型及隐式类型转换的形式化类型语义框架，并给出类型安全条件与五引擎实例化验证。
线性逻辑视角下的 JAX Autodiff
将 JAX Autodiff 编码到线性 λ-演算，证明定性与定量可靠性，并说明 unzipping 可选。
PLEX：精化类型的规范化
提出 PLEX，在 PLE 基础上支持 η-展开、β-归约与依赖模式匹配的符号求值，弥补精化类型与一阶 SMT 求解器间的高阶推理缺口。
当生命周期解放时：面向 arena 的高阶可达性追踪类型系统
提出统一处理多种生命周期、粒度与共享方式的资源类型系统，用可达性类型追踪个体与成组资源，并在 Rocq 中证明类型与内存安全。
CMakeSonar：一种基于细粒度类型系统的 CMake 缺陷静态检测方法
提出首个静态精准检测 CMake 脚本语义缺陷的方法，通过细粒度类型系统与流敏感分析发现构建配置错误。