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
标签：函数式编程（共 254 篇，按优先级展示前 200）
用于贝叶斯编程的仿射单子与惰性结构
提出用于贝叶斯编程的仿射概率单子与惰性结构语义，给出适配惰性的推断方法及 Haskell 库 LazyPPL。
面向模块化贝叶斯推断的函数式编程
提出用函数式语言特性实现模块化概率编程库，可组合出最先进的贝叶斯推断算法。
通过代数效应实现模块化概率模型
提出基于代数效应的嵌入式 DSL，使概率模型模块化、可复用，并统一支持模拟与推断。
在 GitHub 融合工业界与学术界（经验报告）
介绍 GitHub 如何借助函数式编程学术研究构建工业级程序分析工具 Semantic 的经验。
面向离散概率程序推断的随机惰性知识编译
提出随机惰性知识编译，使离散概率程序的精确推断可惰性加速，并用序列蒙特卡洛实现近似推断。
面向无限制代数效应与效应处理的规约与验证
提出 ESL 规约逻辑，支持含命令式效应与高阶构造的零/单/多射效应处理器验证。
LazyHMC：面向惰性、无限维概率程序的 Hamiltonian Monte Carlo 模拟
提出在惰性函数式概率程序中实现无限维参数空间上的梯度型 HMC 与 NUTS，并用 PACAP 分析保证梯度有限支撑。
使用 Idris 进行类型驱动开发
介绍 Idris 中依赖类型驱动的开发方法，面向工程师，涵盖函数式编程、依赖类型与程序验证。
异常异步会话类型：无需层级（tiers）的会话类型
首次将异步会话类型与异常处理集成到函数式语言，给出核心演算与 Links 实现。
面向忙碌程序员的 QuickSpec 快速规范
提出 QuickSpec 的新理论探索架构，通过测试 Haskell 程序自动发现更复杂、更快的等式性质与引理。
可解释自身执行的命令式函数式程序
将动态切片与 Galois 连接扩展到含引用和异常的命令式函数式程序，并证明其正确性与最优性。
面向效应处理器（effect handlers）的分离逻辑
提出内建支持浅层与深层效应处理器的分离逻辑，实现局部推理并基于 Iris 完成模块化验证。
PropR：基于属性的程序修复
将属性测试与 Haskell 类型系统引入自动程序修复，降低过拟合补丁比例并加快修复速度。
通过 Call-by-Push-Value 为函数式程序提取递推式
以 Call-by-Push-Value 为中间语言，从高阶递归函数式程序自动提取运行时间递推式，并给出指称代价语义。
面向高阶函数式语言的半朴素求值
将 Datalog 的半朴素求值扩展到 Datafun 的高阶函数式语言，支持一等关系与高阶函数递归。
CHAD：组合子同态自动微分
提出 CHAD，一种纯函数式、类型保持且可证明正确的前向/反向自动微分源到源变换方法。
Grisette：将符号编译作为函数式编程库
提出纯函数式、静态类型的符号求值库 Grisette，以有序守卫合并路径，显著缩小约束并加速求解。
通过众所周知的程序变换实现高效对偶数反向模式自动微分
提出用线性因子分解等常见函数式程序变换，将对偶数反向模式自动微分优化为复杂度正确且可在 Haskell 中高效实现的算法。
Etna：一个基于属性的测试评估平台（经验报告）
提出 Etna，一个用于经验评估与比较基于属性的测试技术的可扩展平台，并在 Coq 与 Haskell 中开展实验。
证明与反驳函数式编程作业的等价性
用等价性检查自动证明或反驳函数式编程作业的正确性，并通过函数归纳与聚类提升鲁棒性和可扩展性。
工业界的依赖类型 Haskell（经验报告）
报告在 GHC 中编码依赖类型编程的工业经验：可行且有价值，但成本高昂。
高效 CHAD
用稀疏向量、状态传递和去函数化优化 CHAD，使反向模式自动微分达到预期复杂度，并给出 Agda 复杂度证明。
“do”解缚：在纯函数式语言中拥抱局部命令式（函数式珍珠）
为纯函数式语言的 do 记法加入局部可变、提前返回与迭代，并给出到纯函数代码的翻译及 Lean 正确性证明。
高阶需求驱动符号求值
提出 DDSE，一种面向函数式语言的高阶需求驱动符号反向执行，证明其可靠性并用于测试生成。
将基于指针的优化封装在纯函数之后
利用依赖类型将指针地址操作封装为纯接口，使函数式程序保持引用透明并获得图级遍历性能。
实用类型推断中的层级（Levels）
首次系统形式化类型推断实现中广泛使用的 levels 技术，并说明其可用于实际类型推断实现。
非严格语言中的等价性检查
提出基于符号执行与余归纳的演算，自动证明非严格函数式程序等价并生成反例。
混合归纳与余归纳类型的 size-change 原理
将 size-change 原理推广为 totality 检查，以在混合归纳与余归纳类型下可靠验证递归定义。
代数效应在 Cubical Agda 中遇上 Hoare 逻辑
在 Cubical Agda 中用商类型形式化带方程的代数效应，并提供效应通用的 Hoare 逻辑与等式推理。
异构二叉随机访问列表
提出按类型索引的异构二叉随机访问列表，为依赖类型求值器提供支持随机访问的环境表示。
DeCo：一种支持泛型数据类型的增量函数式编程核心演算
提出 DeCo 核心演算，支持泛型数据类型的静态增量函数式编程，并在 Lean 中机械化证明其可靠性。
虚拟化续延
通过虚拟化续延所用的栈空间，在词法效应处理器中完整支持多次性续延，并带来并行执行性能收益。
用逆向处理器为 Arrow 编程反向传播
提出 Arrow 的逆向处理器与范畴语义，使神经网络可符号化构造并通过处理器实现反向传播。
从非递归表达式归纳合成结构递归的函数式程序
提出块级剪枝与版本空间学习，从输入输出示例合成递归函数式程序。
领域特定张量语言
提出嵌入 Haskell 的 EDSL，以索引记法表达张量并用代数结构定义语义。
论带效应答案类型多态程序的高阶模型检测
提出支持答案类型多态与子类型的效应处理演算 HEPCF□ATM，并通过选择性 CPS 变换证明其高阶模型检测可判定。
使用分级模态类型的定量程序推理
提出分级模态类型统一 coeffect 与 graded monad，并在 Granule 中结合线性/索引类型实现定量程序推理。
带类型洞的实时函数式编程
提出带类型洞的不完整函数式程序动态语义，求值可绕过洞并支持填洞后恢复，已在Agda机器化并实现于Hazel。
基于实时双向求值的程序草图
提出 Smyth，用实时双向求值将断言求值产生的示例反向传播，指导类型化函数式程序草图中洞的补全。
函数式数组处理语言中的高效可微编程
在函数式数组处理语言中集成源到源前向自动微分与循环变换等全局优化，使梯度计算效率可与反向模式媲美。
Doo bee doo bee doo
提出严格函数式语言 Frank，用双向效果类型系统与推广的函数抽象统一 effect handlers，并引入 adaptor 支持效果封装与重连。
支持异常的灵活动态信息流控制
提出 LIO：以 Haskell 库形式实现动态信息流控制，用浮动标签与 current clearance 处理异常下的机密性与完整性。
火三角：如何混合替换、依赖消去与效应
提出类型论中替换、依赖消去与效应不相容的 no-go 定理，并给出依赖 CBPV 演算 ∂CBPV 以调和三者。
Effekt：用于 Scala 中类型与效应安全、可扩展效应处理器的能力传递风格
提出 Scala 库 Effekt，以能力传递与交叉/路径依赖类型实现支持效应安全和效应多态、无需类型级编程的效应处理器。
作为幺半群的计算概念
把 monad、applicative functor 和 arrow 统一为 monoidal 范畴中的幺半群，并给出自由幺半群与 Cayley 表示及关系分析。
一种消除依赖成瘾的效应化方法
提出 weaning 翻译，首次在依赖类型论 CIC 中安全引入异常、非终止、非确定性等计算效应。
一种解决七个编程问题的统一方法（函数式珍珠）
提出用 miniKanren 约束逻辑编程统一解决 Racket 中七个编程挑战的优雅方法。
效应处理器：证据翻译
提出 scoped resumptions 限制与证据翻译，证明其可靠一致并实现高效效应处理器。
基于半环字典的函数式集合编程
提出半环字典这一纯函数式集合抽象与静态类型语言SDQL，统一数据库与线性代数优化，高效处理混合工作负载。
强 call-by-need 的基础
提出一种强 call-by-need 求值策略，可计算开放 λ 项的强范式，并用非幂等交类型证明其完备性。
带作用域操作的语法与语义
提出带作用域操作的抽象语法的范畴模型，以分离代数效应与处理器的语法和语义。
基于精确实数算术与连续性的可靠且鲁棒实体建模
提出 StoneWorks 库、MarshallB 语言与 K-rep 表示，使实体建模在精确实数算术和连续性下可靠且鲁棒。
效果、能力与盒子：从基于作用域的推理到基于类型的推理，再返回
提出 System C，将能力与效果系统统一起来，并用盒式值恢复二等值限制，支持完整效应处理器并证明可靠性。
代数效应与处理器不需要值限制
提出可对任意计算泛化的 HM 多态类型系统，证明代数效应与处理器的可靠性，无需值限制。
高阶函数前向自动微分中的扰动混淆
揭示高阶函数前向自动微分中扰动标记失效导致结果错误的微妙 bug，并讨论两种修复方案及其缺陷。
从非递归表达式归纳合成结构递归的函数式程序
提出基于块剪枝的归纳合成方法，从输入输出示例合成结构递归的函数式程序，并在 Trio 系统中达到 98% 的基准求解率。
服务于数百万 Docker 桌面的函数式网络（经验报告）
总结 Docker Desktop 用 OCaml unikernel 在非 Linux 主机上支撑容器网络十年的工程经验。
显式效应子类型
提出显式类型化、带子类型与强制转换的代数效应处理器核心演算及约束推断算法。
基于代数效应的通用事件关联
基于代数效应与处理器，首次统一表达异步事件流上的多种 n 路 join 变体。
Agda 中的交互式编程——对象与图形用户界面
提出 Agda 中基于共归纳 IO 与 copattern 匹配的交互式对象编程方法，实现 ooAgda 库并支持 GUI 与对象验证。
C++ 中的高层效应处理器
提出 cpp-effects 库，在带手动内存管理的 C++ 中实现带类型的高层效应处理器，并验证其性能竞争力。
按需调用即是预见性按值调用
提出用非确定性替代堆状态的预见性求值语义，证明其与标准按需调用语义强等价，并简化推理与给出首个指称代价语义。
选择性应用函子
提出选择性应用函子，介于应用函子与单子之间，可静态声明效果并动态选择执行。
应用式双向编程
提出应用式高阶双向编程框架，让双向变换能以标准函数式语言中的单向程序编写，并桥接 lens 与语义双向化两种方法。
Affect：一种仿射类型与效应系统
提出 Affect：用仿射类型与效应静态追踪续延的 one-shot/multi-shot 用法，并在 Coq/Iris 中证明其可靠性。
解析随机性
用自由生成器统一随机生成与解析，证明生成器可分解为解析器加选择序列分布，并借助导数实现带前置条件的数据生成。
Monad 与 Comonad 的交互定律
提出函子-函子与 monad-comonad 交互定律，统一刻画带效应计算与效应机器行为的交互，并联系有状态 runner。
面向经典逻辑的消耗类型与持久类型
提出消耗与持久类型系统，无需求值即可精确预测带控制算子函数式程序到范式的步数与范式大小。
通过去嵌入实现嵌入
提出“去嵌入”通用策略，将 HOAS 风格嵌入表示转为 de Bruijn 索引项，以支持增量计算与双向变换等语义域。
效应处理器的一等名称
提出将效应处理器名称作为一等值，并借助 scoped effects 与 rank-2 多态防止名称逃逸的命名处理器设计。
尾递归模上下文：一种等式方法
将 TRMc 推广为 TRMC，从规约等式推导通用算法，并在 Koka 实现支持非线性控制的混合版本。
Hefty 代数：高阶代数效应的模块化精化
提出 Hefty 代数，将高阶操作的展开过程模块化，从而在不改接口、不重编译的情况下支持高阶代数效应的实现与精化。
可解释的动态规划
提出基于细粒度值表示解释动态规划结果的方法，并用 Haskell 库支持从递推关系自动生成可解释实现。
并行双数（dual-numbers）反向模式自动微分
提出可高效实现的并行 dual-numbers 反向 AD 技术，能对任务并行源程序生成任务并行导数计算。
面向所有人的模态 FRP：在 Haskell 中无空间泄漏的函数响应式编程
提出并实现 Rattus：一种简化模态类型系统、可浅层嵌入 Haskell 且保证因果性、生产率与无空间泄漏的模态 FRP 语言。
容错函数式反应式编程（函数式珍珠）
为 FRP 抽象引入风险标签与置信度，并用类型级编程提供静态容错保证。
不受束缚的 Visitors
提出 OCaml 的 Visitors 类型导向生成器与 alphaLib 库，使含名字绑定的 AST 遍历与变换可组合、可定制且模块化。
使用 Paramorphism 的递归程序合成
将递归程序合成拆分为固定递归结构的模板与非递归片段搜索，利用 paramorphism 简化并超越已有方法。
为代数效应处理器抽象效应系统
提出参数化于效应代数的类型与效应系统 λ_EA，抽象并统一现有代数效应处理器的效应系统，并证明其类型-效应安全性。
从能力到区域：实现词法效应处理器的高效编译
提出将二等能力推断为区域/证据的提升推断翻译，使词法效应处理器高效编译且保持类型与语义。
在分叉路径的花园中推理
提出基于 clairvoyant call-by-value 的框架与 clairvoyance monad，在 Coq 中机械化推理惰性函数式程序的计算开销。
泛型遍历的泛型派生
提出结合 lens 与 traversal 的泛型派生库，可自动生成高效的数据结构查询与修改遍历。
Daedalus：更安全的文档解析
提出安全解析器 DSL Daedalus，基于函数式解析组合子与流操作构造，可生成多语言安全解析器。
带效应的高效并行函数式编程
提出支持纠缠与任意突变的技术，使并行函数式语言兼顾安全与性能。
程序副词与 Tlön 嵌入
提出程序副词及 Tlön 嵌入，为带效应语言提供比自由单子更灵活且保留更多语法结构的形式语义。
效应换效率：一等控制带来渐近加速
证明效应处理器能为 generic count 带来渐近运行时加速，且该优势无法由可变状态弥补。
通过分数唯一性实现函数式所有权
将分数权限与分级类型结合，使 Rust 式所有权和借用平滑融入支持线性、分级类型的函数式类型系统。
命令式二叉搜索树的函数式本质
提出与命令式版本同速的 move-to-root、splay、zip 树函数式算法，并在 Coq/Iris 中机器验证等价性。
两级类型论中的无闭包函数式编程
提出两级类型论，将依赖类型编译期语言与无闭包一阶对象语言结合，保证抽象不产生运行时闭包。
超越 Relooper：将非结构化控制流递归翻译为结构化控制流（函数式珍珠）
提出单趟递归算法，将任意控制流图翻译为结构化控制流，并计划集成到 GHC。
不止靠等式：用可扩展效应进行推理
提出基于代数可扩展效应的指称语义框架，由程序与处理器诱导等式定律，并证明模处理器等价是同余。
终极条件语法
提出一种支持并行/嵌套匹配与条件模式流动的新型模式匹配语法，可脱糖到无回溯核心并保持语义。
契约透镜：通过计算推理双向程序
提出带谓词契约的 contract lens 与双向计算律，用程序演算从规约推导高效双向变换。
效应处理器的一般细粒度归约理论
提出深度效应处理器细粒度归约理论，给出标准归约策略，证明其保持观测等价，并用于重写优化与NBE规范化。
容错函数式反应式编程（扩展版）
将容错机制引入函数式反应式编程，在值层注入故障并在类型层保证容错性质。
广义幺半效应与处理器
把代数效应与处理器从 monad 推广到广义幺半，统一 monad、applicative 与 arrow 并支持处理器复用。
函数响应式系统的运行时验证与确认
利用纯函数式FRP的引用透明性，为跨平台响应式系统提供断言、记录回放与随机测试结合的运行时验证调试方法。
全规约 Krivine 抽象机 KN 以锁步方式模拟纯正常序规约：基于对应演算的证明
证明改进的全规约 Krivine 抽象机 KN 以锁步方式模拟纯 λ 演算的标准正常序规约。
单子重写系统的关系理论（第一部分）
提出单子重写的关系理论，识别弱笛卡尔单子与线性方程条件，并给出带代数效应的 CBV λ 演算的标准化与合流定理。
Biparsers：面向数据同步的精确打印
提出首个支持非单射解析器精确打印的 biparser 框架，用 lens 统一解析与打印，并实现 JSON/YAML 子集。
Call-by-Push-Value 的抽象操作语义方法
基于预层范畴与高阶抽象 GSOS，为 CBPV 和细粒度 CBV 建立模块化的程序等价推理方法。
模态效应类型
提出基于模态效应类型的新方法，无需显式效应多态即可静态保证效应操作均被处理。
函数式语言中的 Fluent API
提出在无函数名重载的函数式语言中借助参数多态与 Hindley-Milner 类型推断实现编译期检查的 Fluent API。
异步模态 FRP
提出 Async RaTT，一种带异步延迟模态的异步 FRP 语言，并证明因果性、生产性与无空间泄漏等操作性质。
高阶类型中连续性与复杂性的统一框架
提出参数化单子翻译，统一刻画高阶计算中的终止性、连续性与复杂性。
强函数式珍珠：在 Cedille 中实现 Harper 的正则表达式匹配器
在 Cedille 中用递归宇宙接口将 Harper 的续延式正则表达式匹配器实现为强函数式程序，静态保证其全输入终止。
JEDI：Java 声明式与命令式查询的评估
提出 JEDI，一个由 SQL 基准自动生成 Java 基准的套件，用于评测 Java Stream API 并总结高效写法。
OCaml Blockly
开发了理解 OCaml 作用域与类型规则的块编程环境，使完整块程序生成的 OCaml 代码保证可编译。
直接实现多次恢复与局部可变状态
为词法效应处理器提出编译策略与运行时，支持多次恢复与栈分配可变状态，同时保持常数时间捕获/恢复与竞争力性能。
通过效应处理器实现的渐近加速
证明通用效应处理器使 generic count 获得渐近加速，差距源于单次与多次限定控制之别。
并行代数效应处理器
首次将用户定义代数效应处理器与可并行计算结合，给出 λp/Fp 形式化、类型安全证明及 Haskell 实现。
金融市场中的函数式编程（经验报告）
报告渣打银行以 Haskell 构建类型驱动的大规模定价工作流，证明函数式编程可支撑工业级核心业务。
强按需调用的简单高效实现：一种抽象机方法
从 memothunk 求值器自动推导强按需调用抽象机，证明其保守扩展 Krivine 机并以双线性步模拟 normal order。
序列决策问题、依赖类型与通用解
用依赖类型语言给出有限时程序列决策问题的计算机检查通用实现与贝尔曼最优性原理证明。
Let It Be Optimized：用 let 插入与优化以小步构建多阶段求值器（函数式 Pearl）
用扩展 CPS 定义解释器，为库式多阶段求值中的自动 let 插入与优化建立操作语义，并模块化展示多种优化。
并行流式计算的函数式语义
提出核心语言 λ∨，用流序统一函数式编程与确定性分布式计算的基础。
一阶惰性
提出一阶惰性构造子，将惰性数据结构中的 thunk 去功能化，从而提升性能并便于调试。
节点复制：理论与实践
提出实现高阶节点复制的项演算，统一刻画按名调用与完全惰性按需调用并证明两者观察等价。
Galois 连接关联 call-by-value 与 call-by-name
用 call-by-push-value 与 Galois 连接刻画传值与传名的可观察行为关系。
面向 Arrow 的代数效应与处理器
为 Arrow 演算引入代数效应与处理器，给出操作/指称语义，并证明可靠性与充分性。
带效应的软件契约
在效应处理器语境下提出通用效应契约系统，并证明契约不会不当干扰程序执行。
带逻辑等式反射的依赖类型编程
提出 System DE，用模式同时追踪终止性与相关性并支持等式反射，使证明可在编译前被擦除。
二阶计算规则的模块化终止性证明及其在代数效应处理器中的应用
提出二阶计算规则的模块化终止证明方法并实现工具SOL，用于代数效应处理器的CBPV演算终止性。
嵌套类型与 GADT 的参数性
为直接以不动点构造的嵌套类型建立参数模型，推导自由定理，并揭示 GADT 扩展的局限。
更多前驱函数：一次表示法训练
从丘奇数与Kleene表示出发，系统推导出更小、更快、更精确的前驱函数表示。
弱按值调用 λ-演算在时间和空间上都是合理的
证明弱按值调用 λ-演算的 β-归约步数与最大项大小是合理的时间、空间度量，可与图灵机多项式时间、常数空间互模拟。
效果的严格与惰性语义：层叠 monad 与 comonad
构造出一对无法用分配律赋予语义的效果实例，并将其与严格性/惰性对偶联系起来。
用判断性 Monad 律处理高阶效应操作
提出支持高阶效应操作处理器的核心演算，处理器由无律原始 Monad 承载而计算判断满足判断性 Monad 律，并给出语义模型与元定理。
核心函数式语言的惰性线性
提出 Linear Core，将线性资源语义从语法出现扩展到惰性求值语义，并证明其可靠性及优化保持线性。
严格性的类型化
提出更精细的严格性定义，并在按名调用与 CBPV 中建立类型系统，证明其准确刻画变量的运行时使用。
rank-2 多态函数的类字典特化
提出部分求值优化技术，打破递归 rank-2 多态函数无法进行类字典特化的僵局，并在 GHC 插件中实现显著加速。
有效命题（EPR）高阶函数式编程
在高阶纯函数式语言中借助 Extended EPR 与关系抽象实现可判定、支持量词的程序验证，并用三值逻辑隐藏编码复杂性。
Pure Borrow：线性 Haskell 遇上 Rust 风格借用
提出 Pure Borrow，在 Linear Haskell 中以纯函数方式实现 Rust 式借用，支持仿射可变引用的并行突变且保持纯度。
面向幻灯片演示的动画图片：从浅层到深层的领域特定语言（函数式珍珠）
提出一种嵌入式动画幻灯片 DSL，统一深浅嵌入，支持自定义动画组合子并检视、调整和重组动画。
精确地实现不精确概率编程：以分级单子、BDD 与半环参数化推断构造 credal 集（函数式珍珠）
证明不精确概率可直接复用标准 BDD 编译与加权模型计数，并以分级单子实现 Haskell 嵌入式 DSL Imp。
当类型相遇、效应被处理
为带代数效应与处理器的 λ-演算提出首个兼具终止刻画与可达性归约能力的交集类型系统。
方形中有多少？用方形计算函数式程序
提出以（半）交换方形为核心的关系式图形演算，用于计算函数式程序并给出 foldr/foldl 的泛型无归纳理论。
结构余归纳的上下文形式化
提出结构余归纳的上下文形式化，为余递归程序的等式推理提供直观且相对观察等价可靠的证明方法。
《函数式编程杂志》程序计算专刊
《函数式编程杂志》程序计算专刊的条目，未提供摘要，具体贡献无法从所给材料确定。
Hefty 代数：高阶效应的模块化精化
提出 Hefty 代数，用语法重载为高阶代数效应建立模块化精化语义，并在 Agda 中形式化。
面向效应处理器的 Dynamic Wind
为词法效应处理器设计并形式化了一种 dynamic wind，在任意控制效应下保持良定义语义与资源括约。
高阶异步效应
提出高阶异步效应，将操作调用解耦为信号与中断，用核心演算统一异步与代数效应。
从高层到低层：用状态模拟非确定性与状态
用代数效应与处理句柄将 Prolog 式局部状态逐步翻译为低层状态效应，并用程序计算证明各步正确。
超越树：计算基于图的编译器（函数式珍珠）
将编译器计算从树结构扩展到图结构，用高阶抽象语法表示图，从正确性规约推导生成图结构代码的编译器。
可认证的全序列化器及其在 Huffman 编码中的应用
在 Agda 中构造可认证的全序列化器，并以 Huffman 编码作为形式化正确性证明的应用案例。
Simply RaTT：一种用于无空间泄漏反应式编程的 Fitch 风格模态演算
提出 Fitch 风格模态演算 Simply RaTT，保证反应式程序因果性并消除空间与时间泄漏。
带效应的应用性互模拟：单子、relator 与 Howe 方法
在带代数效应的 call-by-value λ-演算中，用 monad 和 relator 抽象推广应用性互模拟，并刻画其成为同余的条件。
白天作绑定器，夜晚作标签：经由词法作用域 handler 实现效应实例
提出用词法作用域 handler 为代数效应实例命名并在类型中追踪，从而在同一上下文中组合同一效应的多次使用。
基于广义续延的效应处理器
为深度、浅层和参数化效应处理器提出基于广义续延的 CPS 变换与 CEK 抽象机实现。
抽象化代数效应
提出 λ_HEL 演算及存在/局部代数效应，用类型化运行时强制转换保障效应抽象不被破坏。
以能力传递风格编译效应处理器
提出能力传递风格与迭代 CPS 编译效应处理器，并用精化类型系统完全消除其抽象开销。
函数式反应式编程的测试与调试
基于纯函数式 FRP 的引用透明性，提出跨平台的时间逻辑断言、记录回放与随机测试方法。
HasChor：面向所有人的函数式编排编程（Functional Pearl）
提出基于 monad 的函数式编排编程模型，支持高阶与位置多态编排，并实现为 Haskell 库 HasChor。
分阶段的选择性解析器组合子
利用解析树、selective functors 和 staging，将解析器组合子编译为手写质量的解析器，并在 Parsley 库中实现。
广义证据传递的效应处理器：将效应处理器高效编译到 C
提出广义证据传递等精化技术，把代数效应处理器高效编译到 C，性能超越多个最佳实现。
用续延编译，还是不用？随便。
提出一种可按需选择 CPS 的新编译器 IR，在直接风格与完全 CPS 间灵活优化续延。
使用自动评估与函数式 Glossy 游戏教授编程（经验报告）
报告五年课程重构经验：以函数式游戏编程、测试驱动开发和自动评估平台提升入门编程教学效果。
关于 Yoneda 你需要知道的：profunctor optics 与 Yoneda 引理（函数式珍珠）
用 Yoneda 引理从具体 getter/setter 表示推导 profunctor optics，阐明 lens/prism 的可组合表示。
让持久化惠及大众：系统语言中的 RRB 向量
提出嵌入式 RRB-Tree 的 C++ 持久向量实现，把持久数据结构与瞬时批量更新引入系统编程。
通过模态刻画代数效应的行为等价
提出用模态逻辑刻画代数效应程序行为等价的一般框架，并证明其与applicative bisimilarity一致且为同余。
钻石并非永恒：守卫递归反应式编程中的活性
提出 Lively RaTT，将 LTL 的时间步模态作为守卫递归的子模态，在保留守卫不动点的同时支持活性类型。
用自动评分教授函数式编程的艺术（经验报告）
扩展 Learn-OCaml 自动评分，使其评价测试质量与代码风格，并分享函数式编程教学经验。
经由伴随的关系代数
用伴随与分级 monad 为关系代数的连接、分组等操作提供范畴论基础，并导向高效实现。
规模化函数式编程教育：OCaml MOOC 的底层实现
介绍 OCaml MOOC 的浏览器开发环境、评分组合子库与静态检查课程导入，并用数据评估其有效性。
FP²：完全原地函数式编程
提出线性完全原地（FIP）演算，证明一类纯函数式程序可无分配、常量栈空间地原地执行，并在 Koka 中实现。
词法作用域效应处理器：直接实现
提出词法作用域效应处理器的编译策略，将高层效应处理翻译为底层栈切换，并在 Lexa 中实现与验证。
用经典连接词进行编译
将极性扩展到 call-by-need 并引入四种对偶移位，用经典连接词编码类型以编译惰性函数语言。
可证明空间高效的并行函数式编程
提出可证明空间高效的并行函数式程序自动内存管理，将线程调度与GC结合，实现O(R*·P)空间与良好伸缩。
面向代数效应与处理器的上下文模态类型
提出 ECMTT，用上下文模态类型内在地追踪代数效应，并把效应处理器视为上下文间可达性见证。
通过融合推理效应交互
提出用 fold/build 融合与 CPS 变换推导效应处理器组合的充分条件，以判定复合处理器语义。
基于协程的 C 语言效应处理器
提出 libseff：面向 C 的基于协程的效应处理器库，可直接在 C 程序中使用且性能有竞争力。
局部代数效应理论
提出类型系统追踪程序局部观察到的代数效应方程，避免全局平凡理论，支持可靠灵活的推理与优化。
如何设计共程序（co-programs）
主张程序设计教学除输入数据结构外也应考虑输出数据结构，从而引导学生写出结构余递归程序。
在 Chez Scheme 上重建 Racket（经验报告）
将 Racket 重建于 Chez Scheme 之上，验证了以其作为目标虚拟机的可行性。
管住你的惰性
提出 StrictCheck，用基于属性的随机测试规定并检验 Haskell 函数的严格性。
泛型函数式并行算法：scan 与 FFT
用和、积与复合等泛型构造统一表达并行 scan 和 FFT，无需数组并揭示算法共性。
代数效应的 Adequacy 再探
为一般（含无穷）代数效应建立基于交互树与单子代数的 CBPV 充分性定理。
异步效应
提出异步代数效应核心演算 λæ，将操作调用解耦为信号与结果中断，并给出类型安全证明与原型。
加权搜索的代数
提出以自由半模 monad 为代数基础的加权搜索框架，并实现 Dijkstra 与高效概率采样。
多态代数效应的签名限制
提出签名限制，通过约束代数效应操作的类型签名，在多态类型赋值下保障多态效应的类型安全。
一个漂亮但不贪婪的美化打印器（函数式珠玑）
提出要求输出全局最短且可任意对齐子文档的美化打印规约，并给出线性时间的非贪婪函数式实现。
ShakeFlow：使用延迟不敏感接口组合子的函数式硬件描述
提出 ShakeFlow，用延迟不敏感接口组合子在函数式硬件描述中组合 valid/ready 等电路。
左折叠与右折叠事关紧要：直接风格、累加器与续延
用左右折叠等价性统一互推导直接风格、累加器与定界 CPS，并厘清其成立条件及列表 fold 参数顺序的影响。
使用 zipper 的解析（函数式珍珠）
将 zipper 从树推广到上下文无关文法，通过挂起遍历状态消除 Parsing with Derivatives 的重复遍历并显著提速。
Pythonic 函数式构造的可理解性研究
通过209名开发者的对照实验，评估Python函数式构造相比过程式写法在可理解性上的差异与使用建议。
命令式与声明式集合处理
随机对照实验表明，Java Stream API 的声明式集合代码在理解速度与正确性上显著优于传统循环。
单子编程中的商：投射代数等价于余代数
证明单子编程中投射代数范畴等价于单子分解所诱导余代数的范畴，从而可用余代数实现多态商类型。
Scoped Effects 与 Handlers 的演算
提出原生支持代数与 scoped effects/handlers 的演算 λ_sc，含多态处理器、转发子句及类型-效应系统与推断。
锁步模拟小菜一碟（经验报告）
在 Haskell 纯度和静态指针支持下，锁步模拟变得极易实现，并可在 CodeWorld 中无纪律要求地提供一致性。
更快的协程管道
提出基于延续的协程管道实现，消除嵌套减速并显著提升通信密集场景性能。
作用域效应、作用域操作与参数化代数理论
将作用域效应翻译为参数化代数理论的变体，给出等式推理与用生成元和方程刻画 monad 的新方法。
当学生切换（函数式）语言时会发生什么（经验报告）
报告新手在已掌握一门语言后学习另一门（函数式）语言时遇到的困难，尤其是持续性问题。
高阶函数的结构化组合与管道组合（经验报告）
经验报告揭示学生组合高阶函数时，结构化组合与管道组合的难度差异，并讨论函数式编程教学启示。
在原生数据类型全集上的实用泛型编程
为 Agda 设计了一个安全易用的数据类型泛型编程库：泛型构造是普通 Agda 函数，可一行特化到原生数据类型。
用生成器生成电路
提出 YieldFSM 硬件描述语言，用生成器抽象表示时钟级时序，并编译为 Mealy 机，在 RTL 与 HLS 之间提供折中。
Real-time MLton：面向实时函数式程序的 Standard ML 运行时
改造 MLton 的运行时（线程、对象模型、GC），使 Standard ML 可用于实时与嵌入式系统。
Peano 数上的左折叠与右折叠
从 Peano 数上的左、右折叠出发，用幂集等标准函数展示折叠模式的定义与推导。
通过重放过去来捕获未来（函数式珍珠）
提出 thermometer continuations，用异常与状态从头重放计算来实现定界续体，并借此表达任意 monadic 效果。
强传值调用是合理的：内爆式共享
提出新抽象机证明强传值调用求值合理，开销线性并以内爆式共享实现指数加速。
经典计算概念与 Hasegawa-Thielecke 定理
为经典逻辑的线性 L-演算建立对话 duploid 语义，并据此证明 Hasegawa-Thielecke 定理。