ICFP（CCF B）（共 374 篇）
202639 篇 · 10(ICFP)
机器生成、机器检查的验证编译器证明（经验报告）
用 Claude Code 智能体从零机械化 CertiRocq 中 ANF 变换的语义保持证明，产出约 6000 行 Rocq 证明，耗时 94.5 小时。
Proofs Promptly：用 AI Agent 进行面向证明的编程（经验报告）
经验报告：配备证明助手与 CLI 的 AI Agent 可自动产出数千行机器检验证明代码，把人类专家的工作压缩到给定问题描述与审查规约。
RunbookFX：面向可执行事故诊断与缓解的类型与效应安全的 LLM 合成
提出类型化函数式 DSL RunbookFX，用乘积效应代数把事故响应安全分解为风险、能力、回滚三维，并以 Coq 机化证明保障 LLM 合成程序的安全性。
异步等待下的尾模优化
将尾调用优化扩展到异步调用，提出 TMA 变换，避免多余任务，并可与 TMC 结合实现并行且空间优化的递归函数。
在你选择的交互式定理证明器中进行组合式神经-信息物理系统验证
提出 Vehicle 的组合式方法，将神经网络验证与符号证明集成到任意交互式定理证明器中。
LazyHMC：面向惰性、无限维概率程序的 Hamiltonian Monte Carlo 模拟
提出在惰性函数式概率程序中实现无限维参数空间上的梯度型 HMC 与 NUTS，并用 PACAP 分析保证梯度有限支撑。
谓词转换器语义的充分性
提出通用框架证明谓词转换器语义相对于操作语义的充分性，覆盖无界递归概率高阶程序。
Package Managers à la Carte：依赖解析的形式化模型
提出 Package Calculus，统一包管理器依赖解析的核心语义，为跨生态依赖表达提供形式化基础。
集合论类型在 Erlang 中的实践（经验报告）
将集合论类型检查器 Etylizer 应用于自身实现，实证其在真实 Erlang 代码中的表达力、可用性与可扩展性。
按需再按需的控制流分析
提出 DoDCFA，一种穷尽式与需求驱动混合的控制流分析，在提升需求驱动 CFA 速度的同时恢复经典 CFA 的适用性，足以支撑内联优化。
免费的断言：将不变式从算法证明转移到实现证明（函数式珍珠）
结合关系 Hoare 四元组与抽象程序断言标注，将算法层不变式转移到实现证明，简化验证。
一种带 work 与 span credit 的并行时间复杂度分离逻辑
提出 Parcas，用 work credit 与 span credit 在并发分离逻辑中模块化验证 fork-join 程序的并行时间上界，并在 Rocq/Iris 中机器化。
HMCFA：面向效应处理器的一种精确且实用的大步骤控制流分析
提出首个实用的效应处理器大步骤控制流分析 HMCFA，用显式存储与双分量时间戳兼顾精度与可处理性。
快速检验重写系统的收敛性（函数式珍珠）
提出基于随机执行迹生成与收缩的 QuickCheck 方法，测试项重写系统的收敛性并高效发现反例。
组合式生成器等价性
为 Hedgehog 生成器建立形式语义，提出受限语言 Hedgehog→ 以获得可组合的分布语义，支持生成器等价证明。
模式穿越（Mode Crossing）
提出模式穿越与模态种类，使 OxCaml 可自动强化模态类型，减少注解并保持无数据竞争。
一个等式与图形化的不动点演算（函数式珍珠）
为不动点演算给出等式规范，并用可行性关系上的弦图提供图形化等式证明，重证滚动、对角、平方、融合与互递归等关键定理。
可编程的基于属性的测试
提出延迟绑定抽象语法，将属性重化为数据结构并与测试执行器解耦，实现可编程的属性测试语言。
用逆向处理器为 Arrow 编程反向传播
提出 Arrow 的逆向处理器与范畴语义，使神经网络可符号化构造并通过处理器实现反向传播。
基于 Iris 的程序逻辑的完备性
首次给出 Iris 程序逻辑完备性证明方法，并在 Rocq 中机器化验证多种逻辑。
一等约束类型：精化、类型推断、近似与终止性刻画
提出一等约束类型系统 FCCT，证明可类型性精确刻画 call-by-name 终止，并给出可终止的近似类型推断。
带类型转换的依赖类型论的合流技术
将合流技术推广到带类型转换的依赖类型论，并在 Rocq 中形式化验证类型与转换检查算法的部分正确性。
Let It Be Optimized：用 let 插入与优化以小步构建多阶段求值器（函数式 Pearl）
用扩展 CPS 定义解释器，为库式多阶段求值中的自动 let 插入与优化建立操作语义，并模块化展示多种优化。
将内联作为空间优化：弱 λ-演算的一个简单时间与空间不变实现
提出弱 λ-演算的实现模型，在按名与按值策略下同时保持时间与空间复杂度不变。
一等隐式多态的另一种类型推断算法
提出基于算法M约束生成与求解、以显式未知多态类型表示实现一等隐式多态类型推断的新算法。
面向幻灯片演示的动画图片：从浅层到深层的领域特定语言（函数式珍珠）
提出一种嵌入式动画幻灯片 DSL，统一深浅嵌入，支持自定义动画组合子并检视、调整和重组动画。
安全第一：如何在编译器计算中安全地忽略不安全行为
提出 skew bisimilarity，放宽编译器正确性规约，使计算编译器时可安全忽略源语言的不安全行为。
相同的余效应，不同的基底：连接两种主流分级类型方法
建立 graded-base 与 linear-base 两类分级 coeffect 系统之间保类型、grade 与操作语义的翻译。
Citrus：超导电子学的代数推理
提出 Agda 嵌入式 DSL Citrus，支持超导电子电路的门等价与代数推理，并证明 PyLSE 无法处理的任务。
抽象机器的双模型与双正交
为抽象机器提出双模型与双正交语义框架，统一证明 CK/CEK 机器的重要性质与模拟关系。
精确地实现不精确概率编程：以分级单子、BDD 与半环参数化推断构造 credal 集（函数式珍珠）
证明不精确概率可直接复用标准 BDD 编译与加权模型计数，并以分级单子实现 Haskell 嵌入式 DSL Imp。
不再「误引」：安全地提取带 IO 的 F* 程序
用关系式引述结合翻译验证，把带 IO 的浅嵌入 F* 程序提取为深嵌入 STLC，并机器验证其满足 RrHP 安全编译准则。
LoCalMem：面向位置寻址与内容寻址内存的类型导向自适应序列化
提出类型导向的统一内存模型 LoCalMem，用显式边界类型统一本地自适应序列化与内容寻址的分布式去重，并证明其可靠性与局部性。
论分级模态类型论中的递归
提出带自然数递归的分级模态类型论，并在 Agda 中形式化证明资源使用计数可靠，且可扩展到信息流非干涉。
当类型相遇、效应被处理
为带代数效应与处理器的 λ-演算提出首个兼具终止刻画与可达性归约能力的交集类型系统。
迈向高阶双代数指称语义
在高阶 abstract GSOS 框架下给出参数化、与语法解耦的双代数指称语义理论。
基于 Möbius 反演的逆扫描（函数式珍珠）
将偏序集上的 Möbius 反演用作逆扫描计算，导出递归规则、系数稀疏性并跨数据结构复用。
一种可连接、可分割的瞬态序列数据结构
提出一种可连接、可分割的瞬态序列数据结构，兼具持久/临时结构并支持高效转换与索引、两端增删。
编辑寄语
介绍 PACMPL 的办刊定位、与 SIGPLAN 的合作关系及其开放获取承诺。
202536 篇 · 9(ICFP)
用生成函数编译
提出以生成函数为编译目标的概率程序精确推断方法，形式化编译并证明其正确性，实现系统 Geni。
高阶语言中的环境共享分析与调用者提供环境
提出基于抽象解释的高阶环境共享分析并形式化，支持调用者提供环境以减少环境分配。
正确性与性能兼顾：从 Agda 到 Futhark
用 Agda 形式化并抽取到 Futhark，使自动微分与 CNN 代码兼具正确性保证和接近 TensorFlow 的性能。
并发概率程序错误概率界的模块化推理
提出首个高阶并发概率程序错误概率界推理的分离逻辑 Coneris，支持随机化逻辑原子性并由 Rocq/Iris 机器化验证。
调用守卫的抽象定义式解释器
CGADI 将抽象推迟到参数化安全性质触发时，使系统化抽象框架能在部分执行中保持完全精确而不失可计算性。
OCaml 一个片段的 формальная 语义与程序逻辑
为 OCaml 的一个含效应处理器的顺序片段建立形式语义与两种程序逻辑。
McTT：一个经过验证的证明助手内核
提出并实现 McTT，一个在 Rocq 中验证、可提取为 OCaml 的 Martin-Löf 类型论内核。
在分离逻辑中验证图算法：一种代数方法的例证
提出用偏交换幺半群及其态射组织图算法的分离逻辑验证，实现上下文局部推理，并简洁验证 Schorr-Waite 与并查集。
服务于数百万 Docker 桌面的函数式网络（经验报告）
总结 Docker Desktop 用 OCaml unikernel 在非 Linux 主机上支撑容器网络十年的工程经验。
使用严格化语法的类型论中的类型论
提出在内涵类型论中严格化 CwF 语法、避免 transport 的方法，并在 Agda 中形式化典范性证明。
直接实现多次恢复与局部可变状态
为词法效应处理器提出编译策略与运行时，支持多次恢复与栈分配可变状态，同时保持常数时间捕获/恢复与竞争力性能。
Frex：依赖类型的代数化简
提出依赖类型代数化简库 Frex，用泛代数结构保证化简模块终止、可靠且完备。
SecRef*：在 F* 中安全共享已验证与未验证代码之间的可变引用
SecRef* 框架让 F* 中已验证代码与未验证代码安全共享可变引用，并用契约与形式证明保证互操作可靠。
几乎公平模拟
提出一族几乎公平模拟关系及演绎系统，用于证明带Büchi公平条件的迁移系统的公平迹包含。
在分离逻辑中推理弱隔离级别
在分离逻辑中形式化读未提交、读已提交与快照隔离三种弱隔离级别，并机器验证MVCC数据库实现满足快照隔离。
带 splice 变量的多阶段编程
提出带 let-splice 绑定的多阶段演算 λ○▷，用上下文模态类型系统支持 splice 变量，并扩展到代码模式匹配。
一阶惰性
提出一阶惰性构造子，将惰性数据结构中的 thunk 去功能化，从而提升性能并便于调试。
软件规约教学（经验报告）
报告以软件规约为中心的一年级课程经验，创建支持契约与性质测试的教学语言，并用学生访谈评估效果。
高阶数学操作语义中的大步语义
在高阶数学操作语义框架中提出抽象大步 SOS，并由高阶 GSOS 推导，证明二者等价。
动态语言的经过验证的解释器及其在 Nix 表达式语言中的应用
提出延迟替换技术，为 Nix 等动态语言给出小型步操作语义与环境解释器，并在 Rocq 中机器化验证其可靠性与完备性。
机器针织的多项式时间程序等价
提出机器针织程序拓扑语义的规范化算法，并证明其正确性与多项式时间，从而判定程序等价。
非累积性下的基于求值的归一化（NbE）
证明基于无类型域模型的 NbE 也适用于非累积宇宙层级，并给出可靠、完备且机器化的基础。
类型宇宙作为 Kripke 世界
论文拆分可变引用的设计空间，区分对过去/未来分配的依赖，并以类型宇宙层级对应 Kripke 世界构造语义，消除类型-世界循环。
初始语义的 2-函子性及其应用
证明以 monoidal 范畴为参数的初始语义具有 2-范畴结构，并据此关联不同变量绑定表示下的模型。
放松！编排式编程的 Semilenient 核心（函数式珍珠）
将函数式编排语言化简为核心 λχ，提出 semilenient 求值策略，把语义精简为十条规则并修正 Chorλ。
有状态语言的双代数推理
提出区分读者与写者的操作语义，使有状态语言可纳入抽象 GSOS 并获得余归纳等价推理。
Fulls 鲜有不同
提出描述列表长度的子语言，支持倍增与指数增长，并给出在可预测域上完备的长度检查算法，经范畴论拉回证明终止。
归并排序的便宜买卖：如何几乎免费地证明归并排序正确且稳定
用关系参数性刻画稳定归并排序，使多种实现的正确性与稳定性证明在 Rocq 中近乎免费。
将会话类型并发编程融入函数式编程
提出 FuSes，将函数式编程与会话类型并发进程演算融合，并支持类型安全元编程优化。
带效应的透镜：在不同 Monad 之间往返
提出一个更通用的带效应透镜框架，两个方向可使用不同 Monad，并保持往返性质与组合性。
依赖类型论中具有动态重数的线性类型（函数式珍珠）
在依赖类型论内嵌线性类型系统，支持动态重数，为更多函数式程序给出精确类型。
渐进类型的稳健动态嵌入
提出渐进类型的稳健动态嵌入准则，要求动态代码嵌入后赋予静态类型时在任意渐进上下文中失败仅源于上下文，并用 Rocq 形式化。
Haskell 绝热 DSL：在量子硬件上求解经典优化问题
提出 Haskell 库 EnQ，以 Traversable/Monad 表达绝热量子计算，并将优化问题编译到量子硬件。
最长上升趋势问题的真正函数式解法（函数式珍珠）
用 Huet zipper 设计纯函数式最长上升趋势算法，兼得渐近最优与实际高效。
逼近随机访问表的信息论极限：以 (1 + 1/σ)⌊lg n⌋ + σ + 9 步遍历 cons 表
提出两种随机访问表变体，将 cons 表任意元素访问的指针遍历上界从 3⌈lg n⌉−5 改进至接近信息论最优。
CRDT 仿真、模拟与表示独立性
将 CRDT 仿真形式化为迁移系统间的弱模拟，刻画保持的性质并证明表示独立性。
202435 篇 · 8(ICFP)
抽象解释器：一种模块化验证的单子方法
提出以自由单子与处理器分层构建抽象解释器，并在 Coq 中模块化验证其可靠性。
错误信用：面向高阶概率程序错误界的有资源推理
提出 Eris 高阶分离逻辑与错误信用，证明高阶概率程序的精确错误概率上界。
基于依赖细化类型系统的高阶概率程序自动验证
提出依赖细化类型系统，将高阶概率程序的多种定量性质验证归约到扩展 CHC 求解，并可复用现有求解器。
面向无限制代数效应与效应处理的规约与验证
提出 ESL 规约逻辑，支持含命令式效应与高阶构造的零/单/多射效应处理器验证。
基于符号语义的 Rust 健全借用检查
证明 LLBC 及其符号语义是底层指针语言的正确抽象，可作为健全借用检查器，并使 Aeneas 支持循环。
两阶段无限/有限低级内存模型：在 LLVM IR 抽象层级上协调整数–指针转换、有限空间与 undef
提出两阶段无限/有限内存模型，统一 LLVM IR 的整数指针转换、有限空间与 undef，并证明精化以支持优化。
CCLemma：E-Graph 引导的归纳等式证明中的引理发现
提出 e-graph 引导的引理发现，使理论探索目标导向，提升归纳等式证明的效率和能力。
JavaScript 正则表达式语义的 Coq 机器化
首次在 Coq 中忠实机器化 ECMA-262 的 JavaScript 正则语义，证明匹配必然终止且安全，并可提取为通过 Test262 的引擎。
通过守卫精化的几乎必然终止证明
提出 Caliper：用保持终止的高阶程序—概率模型精化，经守卫递归与 Löb 归纳证明几乎必然终止。
用导数进行推导：优化高阶流分析的增量不动点
提出静态与动态特化技术优化增量不动点计算，将高阶流分析加速56倍。
一种用于计算机代数的安全低级语言及其形式验证编译器
提出一种介于 C 与 Rust 之间、面向计算机代数底层库的安全低级语言，并用 Coq 证明其安全性及基于 CompCert 的编译器语义保持。
用模态内存管理“氧化”OCaml
以 affinity、uniqueness、locality 三条 mode 轴实现可完全推断、向后兼容的 OCaml 栈分配与原地更新，安全减少堆分配。
依赖幽灵类型免费获得反射
提出 GTT：在依赖类型中加入可安全擦除的 ghost 宇宙，并给出一致性证明、擦除与 equality reflection。
可快照存储（Snapshottable Stores）
提出可快照存储，以近普通引用的开销支持任意可变引用集合的快照与恢复，并用Iris/Coq证明其核心正确性。
为代数效应处理器抽象效应系统
提出参数化于效应代数的类型与效应系统 λ_EA，抽象并统一现有代数效应处理器的效应系统，并证明其类型-效应安全性。
可编译、可扩展的多语言 DSL（函数式珍珠）
提出 Racket 的 syntax-spec 元语言，使 DSL 实现兼得自动宏扩展与编译优化，并重新实现 miniKanren。
两级类型论中的无闭包函数式编程
提出两级类型论，将依赖类型编译期语言与无闭包一阶对象语言结合，保证抽象不产生运行时闭包。
你的惰性函数的一生：面向惰性程序机械化成本分析的双向需求语义
提出双向需求语义，无需特殊程序逻辑即可外延推理惰性程序成本，并在 Rocq 中机化验证摊销与持久性。
使用精化类型的同步编程
提出并形式化 MARVeLus，一个将验证与实现统一的 CPS 同步语言，给出精化类型元理论并在真实系统上执行已验证程序。
带模块函子的分阶段编译
将多阶段编程与 OCaml 模块函子结合，形式化设计并证明类型可靠性与阶段区分。
上下文类型化（Contextual Typing）
将双向类型检查推广为上下文类型化，传播更丰富的上下文信息以减少标注，并用 QTAS 定量刻画可标注性。
并行代数效应处理器
首次将用户定义代数效应处理器与可并行计算结合，给出 λp/Fp 形式化、类型安全证明及 Haskell 实现。
深入理解相继式演算（函数式珍珠）
本文通过实现一个到 λμμ˜-演算的编译器，首次面向编译器开发者介绍相继式演算作为中间语言。
金融市场中的函数式编程（经验报告）
报告渣打银行以 Haskell 构建类型驱动的大规模定价工作流，证明函数式编程可支撑工业级核心业务。
多态程序可实现性的基于示例推理
利用 container morphism 将多态程序转换为可自动推理的形式，从而基于输入输出示例判定多态规约的可实现性。
精化组合逻辑（RCL）
将精化组合问题对应到分离逻辑蕴涵证明，提出RCL并揭示新验证策略。
递归结构化 Actor 契约中对接收者属性的 blame 正确支持
为 Actor 语言提出两种递归结构的新型契约，用于约束消息接收者及其通信行为，并证明 blame 分配的正确性。
去森林化的漫漫长路：一种移除中间数据结构的类型推断与 elaboration 技术
提出 Lumberhack，用子类型推断与 elaboration 融合递归定义，实现通用去森林化，在 nofib 上平均加速 8.2%。
论 CPS 演算的操作理论：面向中间表示的理论基础
为 CPS 演算建立可靠归约语义与简单类型强规范化证明，奠定编译器 IR 的形式理论基础。
超越树：计算基于图的编译器（函数式珍珠）
将编译器计算从树结构扩展到图结构，用高阶抽象语法表示图，从正确性规约推导生成图结构代码的编译器。
按未装箱值调用（Call-by-Unboxed-Value）
提出 Call-by-Unboxed-Value，以原子/复合与装箱/未装箱两轴统一求值序与表示多态，支持未装箱值与多态混用并指导表示无关编译。
渐进索引归纳类型
提出通用框架 Punk，系统探索渐进索引归纳类型的设计空间，统一 eager/lazy cast 归约语义并给出良行为判据。
如何烘焙一个量子 Π
从 rig groupoid 内部语言 Π 的两个副本出发，用范畴构造与计算效应构造计算普遍的量子语言 Quantum Π。
面向代数数据类型的双端位窃取
提出双端位窃取表示法，利用指针高低位为代数数据类型选择非装箱表示并保持统一表示。
函数式、命令式与数独：让好的、坏的和丑的和谐共处（函数式珍珠）
结合函数式编程与 Esterel 式命令式并发，展示用可变状态和多线程也能写出如纯函数式般易理解的数独求解器。
202333 篇 · 7(ICFP)
强化学习的形式化规约与测试
为基于时序差分的强化学习提出形式规约，并以DSL解释器作测试预言机进行基于属性的测试与变异评估。
面向 big-step 抽象解释器的基于组合子的不动点算法
提出可组合的不动点组合子，以系统构造并保证 big-step 抽象解释器分析算法的可靠性。
面向程序验证的模块化、代码特化与零开销抽象
在 F* 的 Low* 工具链中提出语言技术，使高层模块化验证代码可特化并编译为零开销 C 代码。
带宇宙与擦除的分级模态依赖类型理论及其形式化
提出带宇宙与擦除的分级模态依赖类型理论，并在 Agda 中形式化，证明元理论性质与擦除提取的可靠性。
Etna：一个基于属性的测试评估平台（经验报告）
提出 Etna，一个用于经验评估与比较基于属性的测试技术的可扩展平台，并在 Coq 与 Haskell 中开展实验。
通过互模拟实现可信的运行时验证（经验报告）
CopilotVerifier 为 Copilot 编译器输出的 C 监视器生成与源语义互模拟的正确性证明。
通过抽象单子实现灵活的指令集语义（经验报告）
提出用 Haskell 子集和抽象单子编写可复用的指令集语义，以同一核心语义支持测试、交互证明与软硬件模型检测。
高阶性质导向可达性
提出 PDR 的高阶扩展 HoPDR，用于高阶递归函数描述的系统及高阶程序安全性质验证。
显式精化类型
提出 λert 类型理论，让程序员显式嵌入精化性质的证明，从而支持量词和归纳，并用 Lean 4 证明其可靠性。
MacoCaml：分阶段的可组合与可编译宏
提出 MacoCaml，一种结合宏、阶段分离和基于引用的 staging 的 OCaml 编译时代码生成设计，并给出形式化与实现。
Verse 演算：确定性函数式逻辑编程的核心演算
提出 Verse 演算（VC），为确定性函数式逻辑编程提供小步重写语义，并证明良行为项的重写系统合流。
有你或没你：使用效应排除进行编程
提出支持效应排他的类型与效应系统，可直接表达“除指定效应外皆可”的函数，并在 Flix 中实现。
在带依赖分离协议的分布式分离逻辑中验证可靠网络组件
在 Coq 中基于 Aneris 分布式分离逻辑与依赖分离协议，验证了可靠通信库及其上层 RPC 与复制键值存储组件。
特快专递：基于邮箱类型的编程
提出首个融入邮箱类型的编程语言 Pat，并用算法化类型系统静态防范 actor 通信协议错误与死锁。
通过去嵌入实现嵌入
提出“去嵌入”通用策略，将 HOAS 风格嵌入表示转为 de Bruijn 索引项，以支持增量计算与双向变换等语义域。
让位窃取合法：代数数据类型自定义内存表示的编译
提出源类型与内存类型双视角以精确控制 ADT 内存布局，并给出构造/析构与模式匹配的正确编译算法。
带操作幺半群的模块化模型
提出一个范畴框架，模块化地刻画带操作的幺半群的理论与模型，统一代数操作与作用域/绑定操作。
计算并发语言的编译器
基于 choice trees 的 codensity 版本，通过等式推理将并发语言语义系统化地转换为编译器。
效应处理器的一般细粒度归约理论
提出深度效应处理器细粒度归约理论，给出标准归约策略，证明其保持观测等价，并用于重写优化与NBE规范化。
如何评估渐进类型中的 blame，第二部分
理性程序员实验表明，运行时检查单独帮助有限，Natural 检查结合 blame 显著提供更优调试提示。
从第一性原理出发的分离逻辑中的依赖会话协议（函数式珍珠）
用最基础的并发分离逻辑机制分层构造依赖会话协议，并在 Iris/Coq 中机器化验证。
异步模态 FRP
提出 Async RaTT，一种带异步延迟模态的异步 FRP 语言，并证明因果性、生产性与无空间泄漏等操作性质。
带逻辑等式反射的依赖类型编程
提出 System DE，用模式同时追踪终止性与相关性并支持等式反射，使证明可在编译前被擦除。
带回调的内在类型化会话（Functional Pearl）
提出基于回调/控制反转的嵌入式会话类型实现，使应用代码内在类型化、无法破坏线性性，并扩展到分支、递归、多通道等。
及时计算
在Agda中形式化数字电路，将离散信息适时嵌入连续时间信号，并支持组合式正确的计时分析。
HasChor：面向所有人的函数式编排编程（Functional Pearl）
提出基于 monad 的函数式编排编程模型，支持高阶与位置多态编排，并实现为 Haskell 库 HasChor。
FP²：完全原地函数式编程
提出线性完全原地（FIP）演算，证明一类纯函数式程序可无分配、常量栈空间地原地执行，并在 Koka 中实现。
反思随机生成
提出反射生成器，统一随机生成器在收缩、变异等测试数据生产中的多种用途。
可扩展数据类型的泛型编程：或让 Ad Hoc 可扩展数据类型不再 Ad Hoc
提出用行类型统一支持可扩展记录/变体上的泛型编程，并在 System Rω 中形式化与给出指称语义。
当学生切换（函数式）语言时会发生什么（经验报告）
报告新手在已掌握一门语言后学习另一门（函数式）语言时遇到的困难，尤其是持续性问题。
LURK：Lambda，终极递归知识（经验报告）
提出基于 LISP 的 zk-SNARK 语言 Lurk：将程序作为数据送入通用解释器电路，保持证明规模且图灵完备。
记录、映射与结构体的类型化
提出统一支持 struct 与 map 两种用法的记录类型理论，含语义子类型、无回溯子类型判定算法与记录操作类型算子。
更多不动点！（函数式 Pearl）
用不安全的 unsafePerformIO 实现可生产的纯布尔与集合结构，使 Haskell 递归定义不再落入黑洞。
202235 篇 · 6(ICFP)
安全耦合：耦合式精化类型
受概率耦合启发扩展精化类型，在 Liquid Haskell 中验证概率计算的关系性质与机器学习实现。
使用 Kripke 规约单子的经过验证的符号执行（且无需元编程）
提出基于 Kripke 规约单子构造符号执行验证器并证明其可靠性的系统方法，在 Katamaran 中全验证实现。
通过代数效应实现模块化概率模型
提出基于代数效应的嵌入式 DSL，使概率模型模块化、可复用，并统一支持模拟与推断。
在 GitHub 融合工业界与学术界（经验报告）
介绍 GitHub 如何借助函数式编程学术研究构建工业级程序分析工具 Semantic 的经验。
从操作语义自动派生控制流图生成器
提出从操作语义自动合成多种控制流图生成器的理论、算法与工具 Mandate。
Aeneas：通过函数式翻译验证 Rust 程序
提出 Aeneas，将 Rust 程序轻量翻译到纯 lambda 演算，免去内存推理并用定理证明器验证函数正确性。
Multiparty GV：具有经认证无死锁性的函数式多参与方会话类型
提出函数式多参与方会话类型语言MPGV，支持一等端点并保持无死锁性，结果已在Coq中机器验证。
“do”解缚：在纯函数式语言中拥抱局部命令式（函数式珍珠）
为纯函数式语言的 do 记法加入局部可变、提前返回与迭代，并给出到纯函数代码的翻译及 Lean 正确性证明。
分析 3CPS 中的绑定范围
提出 3CPS 中间表示及静态分析，判定变量绑定范围（寄存器/栈/堆），以支持高阶函数式语言的高效编译。
论 Feller 连续性与完全抽象
引入 Feller 连续性，证明连续采样 λ 演算中多种程序等价与上下文等价一致。
Later Credits：面向 later 模态的资源化推理
提出 later credits，将“消除 later 的权利”变为分离逻辑可拥有资源，以突破 later 模态证明困境。
基于两级类型论的分阶段编译
提出用两级类型论（2LTT）实现支持依赖类型与类型级无限制分阶段编译，并给出正确性证明。
搜索纠缠的程序空间
提出等式约束树自动机（ECTA）以紧凑表示子项选择相互纠缠的程序空间，并据此实现高性能 Haskell 合成器 Hectare。
传值调用可解性的理论
系统研究传值调用 λ 演算的可解性，给出多重类型刻画并指出其与传名调用的语义差异。
分层单子解释器的形式推理
扩展 Coq ITree 库，为分层单子解释器提供泛型提升与关系推理框架，消除样板并简化证明。
一种合理渐进的类型论
提出 GRIP，一个扩展 CastCIC、内蕴精度和异常处理的渐进类型论，兼顾规范化与 CIC 保守扩张。
近乎零开销的纠缠检测
提出动态检测并行函数式程序中纠缠的技术，并证明其可靠性且实现近乎零开销。
分级单子的灵活表示
提出灵活分级表示，克服既有分级表示的缺陷，并建立其与一类分级单子的代数保持对应。
高阶区块链语言的随机测试（经验报告）
报告用 QuickChick 对高阶智能合约语言实现进行基于性质的随机测试，验证类型安全与编译器分析可靠性并发现缺陷。
渐进依赖类型编程中的命题相等性
提出支持命题相等性的渐进依赖类型语言，引入等式见证以保持外延相等函数不可区分，并证明类型安全与渐进保证。
帧受限重用的引用计数
提出 drop-guided 重用算法，使引用计数下的对象原地重用更简单稳健，并证明其帧受限性，在 Koka 中获得显著加速。
线性限定类型：能力与唯一性的通用推断
提出线性约束，把隐式线性参数作为限定类型，扩展 GHC 约束求解器自动推断，降低 Linear Haskell 使用负担。
程序副词与 Tlön 嵌入
提出程序副词及 Tlön 嵌入，为带效应语言提供比自由单子更灵活且保留更多语法结构的形式语义。
超越 Relooper：将非结构化控制流递归翻译为结构化控制流（函数式珍珠）
提出单趟递归算法，将任意控制流图翻译为结构化控制流，并计划集成到 GHC。
Multi types 与合理空间
提出多重类型系统，从类型推导中抽取 Space KAM 的空间开销，并捕获其合理空间与时间成本模型。
单子式编译器计算（函数式珍珠）
将编译器正确性推导从仅收敛行为扩展到同时处理发散行为，用部分性单子显式表示发散并支持等式式计算。
引入与消去，左与右
提出四类引入/消去（左/右）规则构成的编程语言设计空间，并用双表达性原则与证明/反驳对偶分析其模块化影响。
面向 FreezeML 的基于约束的类型推断
为 FreezeML 提出基于约束的类型推断，借助新约束语言与确定性栈机求解，并证明终止性和正确性。
强按需调用的简单高效实现：一种抽象机方法
从 memothunk 求值器自动推导强按需调用抽象机，证明其保守扩展 Krivine 机并以双线性步模拟 normal order。
Fitch 风格模态演算的规范化
提出基于求值规范化的语义方法，为 Fitch 风格模态 λ-演算提供模块化规范化证明，覆盖 K/T/4 公理并机器化验证。
高阶函数的结构化组合与管道组合（经验报告）
经验报告揭示学生组合高阶函数时，结构化组合与管道组合的难度差异，并讨论函数式编程教学启示。
在原生数据类型全集上的实用泛型编程
为 Agda 设计了一个安全易用的数据类型泛型编程库：泛型构造是普通 Agda 函数，可一行特化到原生数据类型。
用生成器生成电路
提出 YieldFSM 硬件描述语言，用生成器抽象表示时钟级时序，并编译为 Mealy 机，在 RTL 与 HLS 之间提供折中。
数据类型泛型编程遇上 elaborator 反射
提出基于 elaborator 反射的 Agda 框架，使数据类型泛型程序可直接实例化到原生数据类型与函数。
一种完全唯一的枚举理论
提出适用于正则类型与索引族的泛型枚举器，保证完备、唯一且公平，并尽可能记忆化已枚举值。
202135 篇 · 5(ICFP)
高阶概率对抗计算：范畴语义与程序逻辑
为高阶概率对抗计算建立一元与关系程序逻辑，并在准 Borel 空间范畴中证明可靠性。
LLVM IR 的模块化、组合式且可执行的形式语义
用 Coq 中 interaction trees 的单子解释为 LLVM IR 大型顺序子集建立模块化、可组合且可执行的形式语义。
切入要点：pointful 数组编程的索引集与保持并行的自动微分
提出将数组视为类型化索引集上的函数，并用类型化效应支持可自动并行化原地更新及保持并行的反向自动微分。
Steel：依赖类型并发分离逻辑中的面向证明的编程
在依赖类型语言 F* 中提出 Steel，用五元组 Hoare 逻辑把并发程序与其分离逻辑证明协同开发。
论续延传递变换与期望成本分析
为带概率选择、递归与成本计量的λ演算定义CPS变换，使表达式应用于续延λv.0即得期望成本，并给出可靠的高阶逻辑EHOL推导紧界。
命题即类型与共享状态
将共享可变状态融入会话并发语言的命题即类型线性逻辑解释，并保持安全与活性。
新近单身，乐在其中：用堆片段改进高阶必别名分析
提出堆片段框架，使高阶必别名/环境分析能够通用且稳健地推理递归，并实例化抽象计数分析。
从重写规则推导高效程序变换
提出在 Coq 中从重写规则与辅助数据结构规约半自动推导高效程序变换及其正确性证明的系统。
面向并行 Unix 管道的有序感知数据流模型
提出顺序感知的数据流模型以精确刻画并行 Unix 管道语义，并证明其并行化变换的正确性。
Catala：一种面向法律的编程语言
提出面向成文法的编程语言 Catala，支持一般/例外规则，并用 F* 验证编译器核心步骤，评估中发现官方实现 bug。
GhostCell：在 Rust 中将权限与数据分离
提出 Rust API GhostCell，以 branded types 分离权限与数据，实现无需牺牲性能与并发安全的内部可变性，并在 Coq 中机器化验证其可靠性。
从分离逻辑规约中获得自由定理
提出从抽象分离逻辑规约推导交互迹的自由定理，并证明逻辑原子并发规约蕴含线性化。
CertiCoq 的组合式优化
提出可传递组合的逻辑关系验证框架，支持多趟编译器优化与分离编译，并在 Coq 中验证 CertiCoq 中端管线。
弱内存模型下并发有界队列的形式化验证
用 Cosmo 并发分离逻辑在弱内存模型下形式化验证多生产者多消费者有界队列。
高效树遍历：协调并行性与稠密数据表示
提出 Parallel Gibbon 编译器，在稠密序列化数据表示上实现类型安全的并行树遍历，兼顾密度与并行性。
ProbNV：网络控制平面的概率验证
提出 ProbNV，将 Cisco 配置翻译为带新型类型系统的概率函数式语言，实现可扩展的概率网络控制平面验证。
认证堆操作程序的合成
提出将分离逻辑综合推导系统化翻译为Coq验证器中目标证明的方法，实现对SuSLik生成堆程序的可认证验证。
存在危机已解决：一等存在类型的类型推断
提出双向类型推断算法，在 Haskell 中无需项标注即可推断存在类型的引入与消除，并采用强存在类型。
在语义课程中用混合嵌入跳过绑定器官僚主义（函数式珍珠）
提出混合嵌入的高阶语法编码，在 Coq 语义课程中无需显式变量，消除绑定细节的证明负担。
在分叉路径的花园中推理
提出基于 clairvoyant call-by-value 的框架与 clairvoyance monad，在 Coq 中机械化推理惰性函数式程序的计算开销。
计算依赖类型的编译器（函数式珍珠）
将编译器计算技术推广到依赖类型设置，以支持类型化源语言并保证编译组件类型安全、便于机器验证。
语言的符号微分与自动微分
将形式语言刻画为类型级字符串谓词，并导出正则表达式符号微分与 trie 自动微分两种对偶解析实现。
基于量子物理学家方法的自动摊销资源分析
提出量子物理学家方法，扩展 AARA 类型系统，以更紧界分析栈等非单调资源。
用分裂与对偶分配交类型和并类型（函数式珍珠）
提出直接作用于源类型的交/并/函数子类型算法，基于 duotyping 与可分裂类型，可判定且实现简洁。
Grafs：声明式图分析
提出声明式图分析语言 Grafs 及合成器，自动为五种高性能图处理框架生成高效代码。
带类型区间的更高阶子类型理论
提出带区间 kind 的 F··ω，为 Scala 高阶类型提供统一的子类型理论基础。
广义证据传递的效应处理器：将效应处理器高效编译到 C
提出广义证据传递等精化技术，把代数效应处理器高效编译到 C，性能超越多个最佳实现。
论 JavaScript AOT 编译的性能
设计实现提前编译（AoT）的 JavaScript 编译器，实验表明其速度可与 JIT 竞争且内存占用显著更低。
线性逻辑中的客户端-服务器会话
提出 coexponentials 扩展经典线性逻辑，为客户端-服务器交互建立会话类型系统与编程语言。
面向代数效应与处理器的上下文模态类型
提出 ECMTT，用上下文模态类型内在地追踪代数效应，并把效应处理器视为上下文间可达性见证。
通过融合推理效应交互
提出用 fold/build 融合与 CPS 变换推导效应处理器组合的充分条件，以判定复合处理器语义。
如何评估渐进类型中的归责（blame）
提出首个评估渐进类型归责策略的方法，并发现多数场景下不精确归责与可证明正确的归责同样有效。
加权搜索的代数
提出以自由半模 monad 为代数基础的加权搜索框架，并实现 Dijkstra 与高效概率采样。
Haskell 中的持久软件事务内存
将持久软件事务内存（PSTM）原生集成进 Haskell 运行时，原子管理持久数据并兼容惰性求值与垃圾回收。
面向按值调用隐式多态、带仿射类型的 CPS 变换
提出带仿射类型的新 CPS 目标语言 Λ_open，解决 CBV 隐式多态 CPS 变换的类型保持难题并证明参数性。
202037 篇 · 4(ICFP)
提升期望：用类型自动进行期望成本分析
提出基于类型的概率程序期望执行成本上界分析，支持高阶函数与归纳数据类型，并将推断归约为线性约束求解。
顺序程序的分离逻辑（functional pearl）
提出面向顺序程序分离逻辑的简易机器化形式化，用于教学并覆盖可靠性证明与近期扩展。
Quick Look：非直谓类型推断
提出 Quick Look 设计，在 GHC 中实现非直谓类型推断，使多态类型成为一等公民，且改动局部且兼容现有扩展。
Liquid 信息流控制
提出 Lifty，用 liquid types 静态验证敏感数据信息流策略，并自动合成修复补丁。
使用匹配逻辑定义绑定器的一种通用方法
提出用匹配逻辑统一公理化定义对象语言中的绑定器，并给出保守扩展与模型完备性结果。
面向摊还分析的指称式递推提取
将递推提取扩展到摊还分析，引入带信用标注的仿射中间语言，并证明其到递推语言的指称正确性。
Liquid 资源类型
提出 Liquid 资源类型，用精化类型与潜势标注自动验证函数式程序的精确资源消耗界。
Kind 即调用约定
提出一种新的中间语言，将调用约定编码在类型的 Kind 中，从而兼顾灵活多态与高效静态编译。
Lower your guards：一个组合式的模式匹配覆盖检查器
提出 Lower Your Guards 算法，将模式匹配归约为守卫树，简化覆盖检查，并在 GHC 中实现，提升准确性和性能。
稳定关系与高阶程序的抽象解释
提出未类型化传值 λ 演算的稳定关系指称语义，并据此导出高阶程序模块化关系分析。
高阶需求驱动符号求值
提出 DDSE，一种面向函数式语言的高阶需求驱动符号反向执行，证明其可靠性并用于测试生成。
将基于指针的优化封装在纯函数之后
利用依赖类型将指针地址操作封装为纯接口，使函数式程序保持引用透明并获得图级遍历性能。
以函数式方式实现高性能：关于将高性能优化表达为重写策略的函数式珍珠
提出 RISE 与 ELEVATE 两个函数式语言，用可组合的重写策略描述优化并自动生成高性能并行代码。
基于实时双向求值的程序草图
提出 Smyth，用实时双向求值将断言求值产生的示例反向传播，指导类型化函数式程序草图中洞的补全。
代数子类型的简明本质：让带子类型的主类型推断变得简单（函数式珍珠）
提出 Simple-sub，以更直观的算法实现 MLsub 的带子类型主类型推断，并实验验证两者一致。
效应处理器：证据翻译
提出 scoped resumptions 限制与证据翻译，证明其可靠一致并实现高效效应处理器。
SteelCore：面向带效果依赖类型程序的可扩展并发分离逻辑
在 F* 的效果化依赖类型论中为并发分离逻辑给出语义，并据此构建可扩展的并发验证库。
Cosmo：多核 OCaml 的并发分离逻辑
为多核 OCaml 的弱内存模型构建分层并发分离逻辑 Cosmo，支持从底层到高层的程序验证。
TLC：分布式组件的时序逻辑
提出 TLC 时序程序逻辑，通过降低组件规约支持分布式组件栈的组合式安全性与活性验证，并证明其可靠性。
用余单子和能力恢复纯性
提出余单子类型纪律与能力空间模型，在带效应λ演算中用类型刻画纯表达式并保持等式推理。
Sparcl：一种部分可逆计算语言
提出线性类型语言 Sparcl，以部分可逆为常态，构造性保证程序可逆性并将双射作为特例。
基于项重写的正则语言类型推断
提出以正则语言为类型的类型系统及推断，用项重写与树自动机自动验证树处理高阶函数程序的安全性质。
Kindly Bent to Free Us：以 kind 弯折解放我们
提出 ML 扩展 Affe，以 kind 和约束类型实现线性/仿射资源管理与借用，且无需表达式内线性注解并保留完整主类型推断。
一个带模式匹配与擦除推断的依赖类型演算
提出带模式匹配与擦除标注的依赖类型演算，并给出健全、完全且最优的擦除推断算法。
效应换效率：一等控制带来渐近加速
证明效应处理器能为 generic count 带来渐近运行时加速，且该优势无法由可变状态弥补。
计算聚焦
提出聚焦多态 CBPV 演算，证明计算完备性，并用聚焦语境建立上下文等价与完全抽象。
强函数式珍珠：在 Cedille 中实现 Harper 的正则表达式匹配器
在 Cedille 中用递归宇宙接口将 Harper 的续延式正则表达式匹配器实现为强函数式程序，静态保证其全输入终止。
Duplo：一个 OCaml 链接后优化框架
提出 Duplo 框架，在低层中间表示 LLIR 上对 OCaml 程序及其 C 依赖做跨语言链接后优化，取得约 7% 加速并使代码体积至少减少 15%。
类型系统中模态的统一视角
提出一种统一的模态结构，用于刻画类型化 λ 演算中的多种模态，并给出其元理论。
为 OCaml 加装并行支持
为 OCaml 设计并实现支持多核并行的 mostly-concurrent GC，兼顾单线程向后兼容与多核扩展性。
以能力传递风格编译效应处理器
提出能力传递风格与迭代 CPS 编译效应处理器，并用精化类型系统完全消除其抽象开销。
Scala 逐步推进：在 Iris 中用步进索引逻辑关系证明 DOT 的可靠性
提出 gDOT 演算，并用 Iris 中的步进索引逻辑关系模型在 Coq 中机器化证明了其可靠性。
分阶段的选择性解析器组合子
利用解析树、selective functors 和 staging，将解析器组合子编译为手写质量的解析器，并在 Parsley 库中实现。
一等隐式函数类型的精化
提出面向完全依赖类型理论的一等隐式函数精化算法，借助核心类型论中的函数类型追踪并细化隐式插入信息。
多态代数效应的签名限制
提出签名限制，通过约束代数效应操作的类型签名，在多态类型赋值下保障多态效应的类型安全。
使用 zipper 的解析（函数式珍珠）
将 zipper 从树推广到上下文无关文法，通过挂起遍历状态消除 Parsing with Derivatives 的重复遍历并显著提速。
用半直积组合与分解基于操作的 CRDT
提出基于操作 CRDT 的半直积构造，统一处理并发操作冲突，并借此组合与分解 CRDT。
201939 篇 · 3(ICFP)
Fuzzi：一种面向差分隐私的三层逻辑
提出面向差分隐私的三层逻辑 Fuzzi，打通敏感度类型逻辑与 apRHL，实现自动且灵活的隐私验证。
揭秘可微编程：shift/reset 与倒数第二个反向传播器
揭示反向模式自动微分与定界延续（shift/reset）的联系，并用多阶段编程实现兼顾性能与表达力的可微编程。
Cubical Agda：一种支持 univalence 与高阶归纳类型的依赖类型编程语言
通过 cubical 原语扩展 Agda，使其原生支持 univalence 与高阶归纳类型并保持构造性。
接下来的 700 个编译器正确性定理（函数式珍珠）
提出统一框架，在存在链接的情况下理解、比较并评估各类编译器正确性定理。
Narcissus：从二进制格式构造即正确地推导解码器与编码器
用 Coq 策略从无冗余二进制格式规范自动推导互为逆的解码器与编码器，并重实现网络协议栈。
带续延的并发程序的机械化关系验证
首个全形式化工具，机械化关系验证带 call/cc 与 throw 的并发高阶命令式程序。
效应的谓词转换器语义（函数式珍珠）
为异常、状态、非确定性与一般递归等效应提出统一的谓词转换器语义，并导出精化关系。
一个合理异常的类型论
提出三层 RETT，在完全依赖类型论中首次一致地推理异常项，并提供 Coq 插件 CoqRETT。
合成差分隐私程序
提出基于线性依赖类型系统的类型导向合成算法，自动构造满足隐私约束的随机化差分隐私程序。
从参数性导出简单的非干扰性
利用参数性在构造演算中证明 polyvariant DCC 的非干扰性，并给出 Agda 机械化证明。
从高层推断算法到高效代码
提出编译方法，将含数组隐变量与共轭似然的高层概率推断程序转换为高效代码。
工业界的依赖类型 Haskell（经验报告）
报告在 GHC 中编码依赖类型编程的工业经验：可行且有价值，但成本高昂。
一种高效的类型安全结构化差异比较算法
提出一种线性时间、类型安全的数据类型泛型结构化 diff 算法，最大化共享并提升补丁自动合并率。
使用分级模态类型的定量程序推理
提出分级模态类型统一 coeffect 与 graded monad，并在 Granule 中结合线性/索引类型实现定量程序推理。
面向所有效应的 Dijkstra 单子
提出通用 Dijkstra 单子语义框架，用单子态射为任意单子副作用程序生成验证语义。
函数式数组处理语言中的高效可微编程
在函数式数组处理语言中集成源到源前向自动微分与循环变换等全局优化，使梯度计算效率可与反向模式媲美。
Equations 重装上阵：在 Coq 中进行高层依赖类型函数式编程与证明
提出 Coq 插件 Equations 的新设计与实现，支持依赖模式匹配和良基递归并自动导出高层证明原则。
实现模态依赖类型论
提出并实现带 S4 必然模态的依赖类型论 MLTT🔒，给出基于 NBE 扩展的类型检查算法及其可靠性与完备性证明。
基于精确实数算术与连续性的可靠且鲁棒实体建模
提出 StoneWorks 库、MarshallB 语言与 K-rep 表示，使实体建模在精确实数算术和连续性下可靠且鲁棒。
渐进依赖类型的近似规范化
提出 GDTL，以近似但全的编译期规范化支持渐进依赖类型，并证明类型检查可判定及渐进保证。
用于分离逻辑验证代码完全抽象编译的线性能力
提出以线性能力在运行时表示分离逻辑资源，并构造完全抽象编译器，从而在验证代码与不可信模块边界动态检查契约。
合成对称 lens
将类型导向程序合成扩展到简单对称 lens，借助信息论和用户标注从示例合成 Boomerang lens。
按需调用即是预见性按值调用
提出用非确定性替代堆状态的预见性求值语义，证明其与标准按需调用语义强等价，并简化推理与给出首个指称代价语义。
选择性应用函子
提出选择性应用函子，介于应用函子与单子之间，可静态声明效果并动态选择执行。
函数式-命令式程序的关系代价分析
提出 ARel 类型与效应系统，用类型精化与 Hoare 式三元组追踪可变数组关系，分析函数式-命令式程序相对代价。
Haskell 中依赖类型的角色机制
将角色机制融入依赖类型系统并在 Coq 中证明其可靠性，为 GHC 引入依赖类型奠定基础。
复制数据存储的顺序编程
提出 Carol 语言，利用一致性卫与精化类型，使复制数据存储的操作可模块化、顺序地编程与验证。
高阶多态类型推断的机械化形式化
首次在 Abella 中完整机械化高阶多态类型推断的元理论，并证明可靠、完备与可判定。
类型类解析的连贯性
首次为基于 elaboration 的类型类解析在超类与灵活上下文等非确定性下建立连贯性的形式证明。
Haskell 中的高阶类型级编程
为 GHC 引入不可匹配箭头，支持类型族部分应用，并证明其可靠性。
支持代数化简的 lambda 演算：通过等式推理实现归约并行化
提出 λas 演算，用 δ 抽象在参数到达前做代数化简，为复杂归约的并行化提供等式推理基础。
Simply RaTT：一种用于无空间泄漏反应式编程的 Fitch 风格模态演算
提出 Fitch 风格模态演算 Simply RaTT，保证反应式程序因果性并消除空间与时间泄漏。
闭包转换对空间是安全的
首次形式化证明平坦环境闭包转换保持语义并对时间与空间安全，且计入垃圾回收。
用续延编译，还是不用？随便。
提出一种可按需选择 CPS 的新编译器 IR，在直接风格与完全 CPS 间灵活优化续延。
用自动评分教授函数式编程的艺术（经验报告）
扩展 Learn-OCaml 自动评分，使其评价测试质量与代码风格，并分享函数式编程教学经验。
混合线性与非线性递归类型
提出支持线性与非线性混合类型及递归类型的 LNL-FPC 类型系统，并给出可靠且计算充分的范畴模型。
在 Chez Scheme 上重建 Racket（经验报告）
将 Racket 重建于 Chez Scheme 之上，验证了以其作为目标虚拟机的可行性。
响应式并行中的公平性
为响应式并行程序引入线程优先级与公平调度，提出公平及时调度原则并证明执行与响应时间界。
Lambda：终极子语言（经验报告）
报告以 System Fω 作为编程语言来教授高级类型化函数式编程课程的经验。
201840 篇 · 2(ICFP)
自动微分的简单本质
从简单规约推导通用自动微分算法，特化后得到无图、无磁带、无变异的简洁反向模式 AD。
带连续随机变量与递归的概率语言的上下文等价
为含连续随机变量、scoring 与递归的无类型概率语言给出上下文等价的完整推理原则。
Mtac2：用于 Coq 中反向推理的类型化策略
提出 Mtac2，为 Coq 提供支持反向推理的类型化策略编程语言，可在策略定义期静态排除多类错误。
面向模块化贝叶斯推断的函数式编程
提出用函数式语言特性实现模块化概率编程库，可组合出最先进的贝叶斯推断算法。
抽象解释器的组合式可靠性证明
提出基于共享解释器与 arrow 接口的框架，使抽象解释器的可靠性证明可组合并复用。
抽象抽象机的再函数化：弥合抽象抽象机与抽象定义解释器之间的鸿沟（函数式珍珠）
通过再函数化等语义变换，将小步抽象抽象机系统转化为大步抽象定义解释器，并揭示控制流分析中精确的调用/返回匹配。
MoSeL：面向分离逻辑交互式证明的通用可扩展模态框架
提出 MoSeL，一个通用可扩展的 Coq 框架，将 Iris 证明模式推广到更广泛的分离逻辑。
面向计算机辅助设计编译与反编译的函数式编程
提出函数式CAD语言LambdaCAD及语义保持编译器，并用求值上下文合成算法将网格反编译回可编辑的CAD程序。
基于时间会话类型的并行复杂度分析
提出时间会话类型，将线性逻辑会话类型扩展以局部、组合地分析并发消息传递程序的参数化并行复杂度。
预备，开始，验证！将 hs-to-coq 应用于真实 Haskell 代码（经验报告）
将 Haskell containers 库翻译到 Coq 并验证，证明可验证成熟、未修改的函数式代码。
Futhark 中高阶模块的静态解释：面向大规模的函数式 GPU 编程
为纯函数式数据并行语言 Futhark 设计高阶模块系统，并在 Coq 中形式化其静态语义与编译期消除。
参数多态与操作式改进
提出对时间开销敏感的操作式参数性理论，用于证明程序融合是时间改进。
构建系统 à la carte
提出可执行模块化框架，将构建系统视为设计空间中的点，通过拆解与重组组件来比较并原型化新构建系统。
类型健全性与性能的谱系
提出统一语义框架解释渐进类型中三种类型健全性方法，并系统比较其性能。
类型与作用域安全的带绑定语法宇宙：其语义与证明
提出一个类型与作用域安全的带绑定语法宇宙，可泛型实现遍历并泛型证明其性质。
免费的等价：面向有效传输的单值参数性
提出单值参数性并在 Coq 中实现透明传输框架，使定义与定理可在等价类型间像相等一样迁移。
精化依赖（共）模式匹配
提出依赖（共）模式匹配到良类型 case tree 核心语言的精化算法，并证明其保持用户子句的首匹配语义。
Merlin：OCaml 的语言服务器（经验报告）
介绍 OCaml 语言服务器 Merlin 的设计经验，聚焦增量处理、不完整程序与编辑器交互。
基于代数效应的通用事件关联
基于代数效应与处理器，首次统一表达异步事件流上的多种 n 路 join 变体。
竞争式并行：正确设置优先级
提出模态类型系统与成本模型，统一协作式与竞争式并行，静态防止优先级反转。
合成商透镜
提出商正则表达式与商透镜，并利用规范化定理从示例合成双向变换。
增量式关系透镜
提出增量式关系透镜及变更传播语义，并实现语言级可更新视图，实验显示比非增量方案快数个数量级。
部分静态数据作为代数的自由扩张
用代数自由扩张统一刻画部分静态数据结构，并据此构建常见代数结构的库。
类型转换与开销：协调渐进类型中的安全性与性能
提出静态开销语义与开销推断技术，为渐进类型程序推荐兼顾安全与性能的类型标注。
依赖类型的泛型零开销复用
在 Curry 风格依赖类型论中用恒等函数内部化泛型复用，使非索引与索引数据类型及其程序零开销复用。
容错函数式反应式编程（函数式珍珠）
为 FRP 抽象引入风险标签与置信度，并用类型级编程提供静态容错保证。
泛型遍历的泛型派生
提出结合 lens 与 traversal 的泛型派生库，可自动生成高效的数据结构查询与修改遍历。
使用高阶逻辑编程原型化函数式语言：一篇关于学习 λProlog/Makam 的函数式珍珠
展示如何用 λProlog/Makam 的高阶逻辑编程快速原型化带复杂类型系统的函数式语言实现。
效果的严格与惰性语义：层叠 monad 与 comonad
构造出一对无法用分配律赋予语义的效果实例，并将其与严格性/惰性对偶联系起来。
从嵌入-投影对看 Graduality
将渐进保证重构为 Graduality，并用嵌入-投影对与逻辑关系证明它，类比参数性。
紧致类型标注与分裂界
提出带双计数器的 multi type 系统，为多种求值策略给出精确的求值步数与结果大小分裂界。
使用自动评估与函数式 Glossy 游戏教授编程（经验报告）
报告五年课程重构经验：以函数式游戏编程、测试驱动开发和自动评估平台提升入门编程教学效果。
关于 Yoneda 你需要知道的：profunctor optics 与 Yoneda 引理（函数式珍珠）
用 Yoneda 引理从具体 getter/setter 表示推导 profunctor optics，阐明 lens/prism 的可组合表示。
经由伴随的关系代数
用伴随与分级 monad 为关系代数的连接、分组等操作提供范畴论基础，并导向高效实现。
用依赖类型处理定界延续
为依赖类型语言引入 shift/reset，限制类型依赖并用答案类型多态给出可靠类型系统与保类型 CPS 翻译。
管住你的惰性
提出 StrictCheck，用基于属性的随机测试规定并检验 Haskell 函数的严格性。
可合理编程的字面量记法
提出类型化字面量宏（TLM），让库在 Reason/OCaml 中定义可抽象推理的新字面量记法，并给出类型论形式化。
通过重放过去来捕获未来（函数式珍珠）
提出 thermometer continuations，用异常与状态从头重放计算来实现定界续体，并借此表达任意 monadic 效果。
差在哪里？关于双射相减的函数式珍珠
提出一种从代数视角高层次构造双射之差的方法，避免逐点推理和分别构造正反方向，且不牺牲性能。
用于优化类型导向编译的有限多态
提出有限多态演算与类型宇宙重构，消除多态编译中的类型传递抽象并加速代码。
201745 篇 · 1(ICFP)
概率程序中数组的符号化条件化
将符号化分解算法扩展到概率程序中的数组，实现无需展开循环的提升式条件化。
面向形式验证的元编程框架
在 Lean 中实现面向形式验证的元编程框架，通过反射对象级表达式支持高效编写 tactic 与自动化。
SpaceSearch：用于构建和验证求解器辅助工具的库
提出 Coq 库 SpaceSearch，让用户在证明助手中构建并验证求解器辅助工具，再提取到 Rosette 高效执行。
嵌入 F* 的经过验证的低层编程
提出 Low*：将良行为 C 子集浅嵌入 F*，以类型保证内存安全并借助 F* 验证，经抽取编译到 C。
抽象定义解释器（函数式珍珠）
提出以定义解释器作为高阶语言抽象解释的基础，并发现抽象定义解释器能自然继承下推控制流精度。
面向复杂度分析的自动化 sized 类型推断
提出一种基于 sized 类型推断、ticking 单子变换与约束求解的全自动高阶函数式程序复杂度分析方法。
可解释自身执行的命令式函数式程序
将动态切片与 Galois 连接扩展到含引用和异常的命令式函数式程序，并证明其正确性与最优性。
局部精化类型化
提出 FUSION 算法实现局部精化类型推断，用 SMT 验证多态数据类型与高阶函数，显著减少模板并加速。
使用 Coq 原型化查询编译器（经验报告）
报告用 Coq 证明助手原型化查询编译器并移植到 Java 的工业经验与利弊。
Kami：面向高层参数化硬件规范及其模块化验证的平台
Kami 是 Coq 库，支持以 Bluespec 风格高层参数化地规范、实现并模块化验证硬件设计。
会话类型中的 Manifest 共享
将共享机制引入会话类型语言，通过线性/共享分层与模态算子，在保持会话保真性的同时允许共享进程竞争导致的死锁。
论用户自定义效应的表达能力：效应处理器、单子反射与定界控制
比较效应处理器、单子反射与定界控制的表达能力，证明类型保持下效应处理器无法被后两者宏表达。
免费的自由定理：有类型与无类型下的参数性
提出改进的多态 blame 演算，用步进索引 Kripke 逻辑关系证明关系参数性，并导出两个自由定理。
带联合与交集类型的渐进类型
为带渐进类型及并集/交集类型联结词的函数式语言建立可靠类型系统，并将子类型判定线性归约到非渐进情形。
Haskell 中依赖类型的规范
为 Dependent Haskell 提出核心语义与显式类型语言，并在 Coq 中形式化类型安全及相关定理。
高阶程序的关系逻辑
提出关系高阶逻辑 RHOL，用于证明高阶程序的关系性质，并统一嵌入多种关系精化类型系统。
依赖类型理论中的参数化量词
为 MLTT 引入参数化量词 ∀ 与 ∃，使参数化定理可在类型系统内部证明，并在 Agda 中实现。
自适应差分隐私框架
提出基于隐私过滤器与类型化函数式编程的自适应组合框架，并实现语言 Adaptive Fuzz，以收紧隐私预算界。
编译到范畴
将类型化函数式程序经保持语义的变换编译到不同范畴，以统一实现硬件电路、自动微分、增量计算等解释。
效应驱动的编译器 QuickChecking
提出类型与效应系统保守检测求值顺序依赖，并据此生成程序以差分测试 OCaml 编译器后端。
面向大小依赖类型的基于求值的规范化
提出整合高阶大小多态与依赖类型的大小类型理论，并用 NBE 判定判等、子类型和类型检查。
一种解决七个编程问题的统一方法（函数式珍珠）
提出用 miniKanren 约束逻辑编程统一解决 Racket 中七个编程挑战的优雅方法。
强 call-by-need 的基础
提出一种强 call-by-need 求值策略，可计算开放 λ 项的强范式，并用非幂等交类型证明其完备性。
渐进会话类型
提出 GradualGV，将动态类型与 cast 引入函数式会话类型系统 GV，统一静态与动态会话处理并保证类型、通信与 blame 安全。
Whip：面向现代服务的高阶契约
提出 Whip 高阶契约系统，用面向服务的高阶契约语言和本地运行时监控，检测服务是否遵守声明的接口。
验证 CakeML 中的高效函数调用
为 CakeML 编译器设计支持函数调用优化的中间语言语义，并在 HOL4 中验证其编译步骤。
如何证明你的演算是可判定的：二阶代数理论与计算的实践应用
提出用二阶代数理论证明演算等式理论可判定的通用方法，并实现 Haskell 工具 SOL 辅助合流性与强规范化证明。
通过语法糖推断作用域
提出作用域推断，将核心语言的作用域规则提升到表面语言，并证明脱糖保持 α-等价。
不受束缚的 Visitors
提出 OCaml 的 Visitors 类型导向生成器与 alphaLib 库，使含名字绑定的 AST 遍历与变换可组合、可定制且模块化。
论多态渐进类型
研究参数多态的渐进类型，提出 System F_G 及其多态 blame 演算翻译，并证明若干 refined criteria。
分阶段泛型编程
用多阶段编程将 Scrap Your Boilerplate 改造成带类型的优化代码生成器，消除泛型编程的性能开销。
函数式反应式编程的测试与调试
基于纯函数式 FRP 的引用透明性，提出跨平台的时间逻辑断言、记录回放与随机测试方法。
让持久化惠及大众：系统语言中的 RRB 向量
提出嵌入式 RRB-Tree 的 C++ 持久向量实现，把持久数据结构与瞬时批量更新引入系统编程。
高阶会话的监护契约
将 chaperone 契约扩展到会话，在高阶语言中建立动态监控语义与 blame 定理，并给出 OCaml 实现。
规模化函数式编程教育：OCaml MOOC 的底层实现
介绍 OCaml MOOC 的浏览器开发环境、评分组合子库与静态检查课程导入，并用数据评估其有效性。
制作电影的 Super 8 语言（函数式珍珠）
通过为视频编辑构建分层 DSL，展示 Racket 教条如何自然导向语言层级并复用宿主语言与类型检查 DSL。
受约束的类型族
用限定类型为类型族计算标注定义域，在保持表达力与类型安全的同时支持偏性，并给出闭类型族语言的一致性证明。
泛型函数式并行算法：scan 与 FFT
用和、积与复合等泛型构造统一表达并行 scan 和 FFT，无需数组并揭示算法共性。
一个漂亮但不贪婪的美化打印器（函数式珠玑）
提出要求输出全局最短且可任意对齐子文档的美化打印规约，并给出线性时间的非贪婪函数式实现。
锁步模拟小菜一碟（经验报告）
在 Haskell 纯度和静态指针支持下，锁步模拟变得极易实现，并可在 CodeWorld 中无纪律要求地提供一致性。
更快的协程管道
提出基于延续的协程管道实现，消除嵌套减速并显著提升通信密集场景性能。
通过操作语义实现更好的生活：面向无线协议的优化编译器
为 Ziria 无线协议语言建立核心语言、操作语义与类型系统，并据此提出融合与流水线合并变换，实现更快的编译器。
无需动脑的 CPS 转换（函数式珍珠）
提出线性时间 CPS 转换算法，不引入行政归约项，输出在 no-brainer 归约系统下即为范式。
Herbarium Racketensis：林间漫步（函数式珍珠）
通过用 Racket 实现 Lindenmayer 系统 DSL，展示 Racket 作为快速构建领域特定语言的抽象平台的能力。
编辑寄语
这是一则欢迎读者阅读 PACMPL 论文集的编辑寄语，不包含具体程序语言研究贡献。