JFP（CCF B）（共 172 篇）
20261 篇 · vol.35
模式合一的语义
提出广义元变量语法与范畴语义，证明特定条件下 Miller 模式合一算法可推广，并用 Agda 实现。
202521 篇 · vol.35
依赖类型论中单子等式推理的实用形式化
在 Coq 中以接口方式形式化效应单子层级与代数律，使单子等式推理可机器化并实用化。
从非递归表达式归纳合成结构递归的函数式程序
提出块级剪枝与版本空间学习，从输入输出示例合成递归函数式程序。
领域特定张量语言
提出嵌入 Haskell 的 EDSL，以索引记法表达张量并用代数结构定义语义。
并行双数（dual-numbers）反向模式自动微分
提出可高效实现的并行 dual-numbers 反向 AD 技术，能对任务并行源程序生成任务并行导数计算。
OCaml Blockly
开发了理解 OCaml 作用域与类型规则的块编程环境，使完整块程序生成的 OCaml 代码保证可编译。
选择树：在 Rocq 中表示并推理非确定性、递归和不纯程序
提出 Rocq 中的 Choice Trees monad，用于统一建模非确定、递归和不纯程序，并复用 LTS 的互模拟与精化工具。
在线性代数中使用图形语法的无点计算式证明与程序推导
展示图形线性代数如何以无点计算式风格统一处理矩阵、向量空间和线性关系，并推导算法与性质。
迈向类型导向的编译器推导
从内在类型化解释器出发，以类型导向的方式推导抽象机与编译器，并为简单表达式语言及STLC优化求值器展示该方法。
方形中有多少？用方形计算函数式程序
提出以（半）交换方形为核心的关系式图形演算，用于计算函数式程序并给出 foldr/foldl 的泛型无归纳理论。
结构余归纳的上下文形式化
提出结构余归纳的上下文形式化，为余递归程序的等式推理提供直观且相对观察等价可靠的证明方法。
二分查找——往好处想
在 Agda 中讲解程序验证的教程，并以二分查找为例展开。
《函数式编程杂志》程序计算专刊
《函数式编程杂志》程序计算专刊的条目，未提供摘要，具体贡献无法从所给材料确定。
Hefty 代数：高阶效应的模块化精化
提出 Hefty 代数，用语法重载为高阶代数效应建立模块化精化语义，并在 Agda 中形式化。
自动测试 Haskell 学生提交的控制台 I/O 行为
提出描述 Haskell 控制台 I/O 交互行为的规约语言与自动测试框架，并用约束求解器生成有意义的输入序列。
传值调用与传名调用：经典定理的一个简单证明
提出轻量级归纳方法，为传值调用可被传名调用模拟这一经典定理给出简单证明。
单子的图形理论
用弦图给出单子的形式理论，使 Eilenberg–Moore/Kleisli 分解、提升与分配律等可用图形化计算统一推导。
模上下文的尾递归：一种等式推导方法（扩展版）
将尾递归模 cons 推广为模上下文，用等式推导出通用 TRMC 算法，并在 Koka 中实现可适应非线性控制的混合版本。
你可以发明 Fenwick 树
用等式推理从段树导出 Fenwick 树，并用 Haskell EDSL 揭示其位运算原理。
评 Vitaly Bragilevsky 的《Haskell in Depth》，Manning Publications，2021
对《Haskell in Depth》的书评；摘要缺失，具体评价无法从元数据获知。
Turner、Bird、Eratosthenes：一条永恒燃烧的线索
以 Bird 的循环埃拉托斯特尼筛为例，探讨其生产性证明，并把它作为 Turner 总体函数式编程的挑战问题。
早期评估在函数式编程教学中的经验
报告在本科一年级函数式编程课中采用“使用-修改-创造”脚手架进行早期评估干预的经验，Create 作业平均提高约 9%。
202414 篇 · vol.34
渐进类型中的静态归责（Static Blame）
提出 Static Blame 框架，静态揭示渐进类型程序中隐藏的数据流并刻画其运行时影响。
一个目标导向的计算式证明示例
通过构造星根，以目标导向的计算式证明建立由关系生成等价关系的自反性与传递性，并联系强连通分量算法。
Alice 还是 Bob？编排中的进程多态
提出 PolyChorλ，首个支持类型与进程多态的高阶函数式编排语言，可在运行时确定参与者并保持投影程序无死锁。
Sparcl：一种用于部分可逆计算的语言
提出线性类型语言 Sparcl，以部分可逆为常态，在构造上保证程序可逆性并提升表达力。
通过效应处理器实现的渐近加速
证明通用效应处理器使 generic count 获得渐近加速，差距源于单次与多次限定控制之别。
共享状态 actor 的编程与推理
提出 facet 记法，为可受控共享状态的 actor 语言提供理论、类型系统与行为类型系统，并报告实现经验。
面向 Arrow 的代数效应与处理器
为 Arrow 演算引入代数效应与处理器，给出操作/指称语义，并证明可靠性与充分性。
从高层到低层：用状态模拟非确定性与状态
用代数效应与处理句柄将 Prolog 式局部状态逐步翻译为低层状态效应，并用程序计算证明各步正确。
一个用于显式空值的简单 blame 演算
提出更简单正交的显式空值 blame 演算，用标准方式证明 blame 定理并支持开放项互嵌。
《函数式编程杂志》对 Sandy Maguire《代数驱动设计》（Leanpub，2020）的书评
这是 JFP 对《Algebra-Driven Design》一书的书评，暂无摘要可供概括其具体内容。
使用子列表树的自底向上计算
为 Bird 的列表自底向上计算算法给出形式推导，并揭示其依赖的 Pascal 三角对角线性质。
渐进类型的类型导向操作语义
提出类型导向操作语义（TDOS），直接给出渐进类型语言的语义，避免经强制转换演算间接编码。
评《Real World OCaml：面向大众的函数式编程》第二版，作者 Yaron Minsky 与 Anil Madhavapeddy，2023
评述《Real World OCaml》第二版，一本面向实践的 OCaml 函数式编程著作。
图解 Knuth–Morris–Pratt
用函数式编程技巧逐步图解推导 KMP 字符串搜索算法，降低理解难度。
202313 篇 · vol.33
轨迹契约
提出轨迹契约，用谓词约束多次函数调用与返回间的值序列，弥补传统行为契约表达力不足。
模态依赖类型理论的求值规范化
提出模态依赖类型论 Mint，并给出其模块化、可机化的求值规范化证明与算法。
契约透镜：通过计算推理双向程序
提出带谓词契约的 contract lens 与双向计算律，用程序演算从规约推导高效双向变换。
Coq 的 sized typing 实用吗？
提出 CIC* sized type theory 与 size inference 并实现于 Coq 内核，评估发现性能严重退化，结论不实用。
从 λ 演算到组合子逻辑的正确构造转换
给出从良类型 λ 项到组合子逻辑的转换，并在静态层面同时保证类型保持与转换正确性。
读/写可因子化程序
通过类型系统区分只可析构与只可构造的数据，提出 RW-可因子化程序，将 cons-free 范式扩展到函数复杂度类。
可认证的全序列化器及其在 Huffman 编码中的应用
在 Agda 中构造可认证的全序列化器，并以 Huffman 编码作为形式化正确性证明的应用案例。
使用 Coq 证明助手推理递归程序的折叠-展开引理——勘误
该文是《使用 Coq 证明助手推理递归程序的折叠-展开引理》的勘误，摘要不可用，无法概括新贡献。
左折叠与右折叠事关紧要：直接风格、累加器与续延
用左右折叠等价性统一互推导直接风格、累加器与定界 CPS，并厘清其成立条件及列表 fold 参数顺序的影响。
编程语言语义：如 1、2、3 般简单
以仅含整数与加法的极小语言为教学载体，简明介绍编程语言语义的核心概念。
经典（余）递归：机制
为原始余递归建立与递归对等的计算基础，借抽象机与逻辑对偶揭示求值策略对（余）递归组合子复杂度的影响。
Featherweight Generic Go 中方法重载与结构化子类型的类型指导、字典传递翻译
提出将 FGG− 类型指导翻译为无类型 lambda 演算，用字典传递实现方法调用解析，并证明语义保持与一致性。
使用 thinning、记忆化和多项式计算布尔函数的 level-p 复杂度
实现了一个纯函数式库，用于计算布尔函数的 level-p 复杂度，并应用于两级迭代多数函数，改进了先前结果。
202214 篇 · vol.32
在 Coq 中从 Coq 提取函数式程序
在 Coq 内构建认证提取管线，将依赖类型程序翻译为多种函数式语言并验证关键变换。
指称语义作为函数式语言代价递推提取的基础
以指称语义形式化函数式程序的代价递推提取：先用单子翻译提取代价，再借不同模型刻画不同的规模概念。
面向所有人的模态 FRP：在 Haskell 中无空间泄漏的函数响应式编程
提出并实现 Rattus：一种简化模态类型系统、可浅层嵌入 Haskell 且保证因果性、生产率与无空间泄漏的模态 FRP 语言。
迁移渐进类型
提出 migrational typing，高效计算渐进类型程序中所有动态到静态类型的替换方式，支持自动迁移与最小动态类型修复。
同步迭代多个集合
提出 Synchrony 迭代抽象，使多有序集合的同步迭代和通用数据库连接可用推导式表达。
ANF 在外延相等意义下保持依赖类型
首次为依赖类型提出带 join-point 优化的 ANF 翻译，并证明其类型保持及分离编译正确性。
使用 Coq 证明助手推理递归程序的折叠–展开引理
提出折叠–展开引理，在 Coq 中机械生成并精确推理局部或全局递归函数，且已由插件支持。
Fregel：一种面向顶点中心大规模图处理的函数式领域特定语言
提出纯函数式DSL Fregel，以组合式图函数编写顶点中心程序，并编译到Giraph/Pregel+。
回到 future
基于伴随逻辑的类型论统一编码 future、fork/join 与单子并发，并给出线性 future 的形式化基础。
超自然数
论文提出/探讨 super-naturals，但提供的英文摘要缺失，无法确定其核心贡献。
幺半群的一种众所周知表示及其在函数“vector reverse”中的应用
利用幺半群的经典表示，使 vector reverse 等依赖类型函数无需额外等式证明即可通过类型检查。
作为 Robert Harper 的博士生
本文是 Robert Harper 纪念文集前言，介绍其核心研究主题并汇编其博士生的回忆，以致敬其 64 岁生日。
先发给我：同步消息传递中的优先级
提出支持选择性通信与一等通信协议的同步消息传递分层优先级方案，并在 CML 中实现验证。
编者按
该文为编者按，未提供摘要，无法归纳具体研究贡献。
202125 篇 · vol.31
论单子式逆向归纳的正确性
定义单子式 SDP 的正确性，给出三个条件证明单子逆向归纳正确，并在 Idris 中形式化。
外延相等保持与已验证泛型编程
提出外延相等保持原则，在内涵类型论中无需扩展理论或完整 setoid 即可进行已验证泛型编程。
函数式-命令式环境下的关系成本分析
提出类型-效应系统 ARel，借助跟踪可变数组关系的类型精化，形式化推导函数式-命令式程序间的相对求值成本界。
参数化转换演算与可复用的渐进类型lambda演算元理论
提出两个参数化转换演算与可复用元理论，统一渐进类型lambda演算变体并在Agda中机械化。
用于概率与非确定性公理化推理的可信 monad
在 Coq 中形式化几何凸单子，为概率与非确定性选择的等式推理提供可信模型和可复用理论。
Cogent：唯一性类型与认证编译
提出函数式语言 Cogent，其唯一性类型系统无需运行时或 GC 即可保证内存安全，并通过双语义与精化定理实现生成 C 代码的认证编译。
驯服 Merge 运算符
提出类型导向操作语义，使带 merge 运算符的不相交交集类型演算具备确定性、主语归约并支持递归。
准备，Set，验证！将 hs-to-coq 应用于真实世界 Haskell 代码
把 hs-to-coq 应用于 Haskell containers 库，验证其类型类定律与接口，并扩展 partiality 支持。
可解释的动态规划
提出基于细粒度值表示解释动态规划结果的方法，并用 Haskell 库支持从递推关系自动生成可解释实现。
集成区域内存管理与无标签分代垃圾回收
提出区域内存管理与无标签分代 GC 的集成方案，并在 MLKit 中实现和评测。
不止靠等式：用可扩展效应进行推理
提出基于代数可扩展效应的指称语义框架，由程序与处理器诱导等式定律，并证明模处理器等价是同余。
高阶函数与 Brouwer 论题
用效应强制证明 System T 中可实现的 bar 满足 Brouwer 单调 bar 定理，并以对话树刻画其构造。
混合敏感度并发程序的验证式安全编译
在 Isabelle/HOL 中验证编译器对混合敏感度并发程序保持非干涉性，并完成到 RISC 风格汇编的安全编译。
面向归约并行化的代数化简 Lambda 演算：扩展研究
提出带代数化简的简单类型 λ 演算 λ_AS，用 δ 抽象和类型系统为复杂归约的并行化提供等式推理基础。
用于分布式系统建模、测试与执行的协议组合子
提出分布式协议组合子 DPC，用声明式程序原语统一分布式系统的建模、测试与执行。
一种删除数字的贪心算法
通过谓词逻辑、依赖类型证明助手和等式推理，系统推导出删除 k 位数字使结果最大的线性时间贪心算法。
最长平衡括号段：一个段问题中的程序反转练习
通过程序反转与段问题技术，线性时间求最长平衡括号段，并推导出移进-归约解析实例。
证明导向的程序变换：高效正则表达式匹配的函数式阐释
通过证明导向的程序变换，从正则表达式集合语义系统推导出高效的表驱动匹配器，并机器验证每一步等式正确性。
归咎与强制转换：首次再度携手
系统构建四种渐进类型演算及其翻译，证明翻译完全抽象，统一归咎与强制转换理论。
如何设计共程序（co-programs）
主张程序设计教学除输入数据结构外也应考虑输出数据结构，从而引导学生写出结构余递归程序。
StkTokens：利用线性 capability 强制良括号控制流与栈封装
提出并形式化 StkTokens 调用约定，用线性 capability 在能力机器上保证良括号控制流与局部状态封装。
Real-time MLton：面向实时函数式程序的 Standard ML 运行时
改造 MLton 的运行时（线程、对象模型、GC），使 Standard ML 可用于实时与嵌入式系统。
可组合的数据可视化
探讨如何以可组合的方式构建数据可视化，并以双值柱状图与共享 x 轴的双折线图作为示例。
Segments：降雨问题的一个替代方案
提出 Segments 问题作为研究函数式程序员解题策略的替代性挑战，并归纳出七种高层解法策略。
什么是教育论文？
说明 PL 教育轨道的定位，并解释将 Education Pearl 更名为 Education Matters 的愿景。
202026 篇 · vol.30
使用 Idris 进行类型驱动开发
介绍 Idris 中依赖类型驱动的开发方法，面向工程师，涵盖函数式编程、依赖类型与程序验证。
异构二叉随机访问列表
提出按类型索引的异构二叉随机访问列表，为依赖类型求值器提供支持随机访问的环境表示。
构建系统 à la carte：理论与实践
提出可执行框架，将构建系统拆解为可组合组件，以系统比较并原型化新的构建系统。
Doo bee doo bee doo
提出严格函数式语言 Frank，用双向效果类型系统与推广的函数抽象统一 effect handlers，并引入 adaptor 支持效果封装与重连。
Effekt：用于 Scala 中类型与效应安全、可扩展效应处理器的能力传递风格
提出 Scala 库 Effekt，以能力传递与交叉/路径依赖类型实现支持效应安全和效应多态、无需类型级编程的效应处理器。
紧致类型与分裂界（完整版）
通过带计数器的多重类型系统，为多种求值策略给出精确的求值步数与结果规模界。
显式效应子类型
提出显式类型化、带子类型与强制转换的代数效应处理器核心演算及约束推断算法。
avoidance 问题的一种聚焦式解决方案
用聚焦逻辑为 ML 模块类型论中的 avoidance 问题建立存在签名元理论，并在 Coq 中形式化。
容错函数式反应式编程（扩展版）
将容错机制引入函数式反应式编程，在值层注入故障并在类型层保证容错性质。
计算正确编译器 II：寄存器机归来
将直接从正确性规约计算编译器的方法从栈式目标机扩展到寄存器机。
广义幺半效应与处理器
把代数效应与处理器从 monad 推广到广义幺半，统一 monad、applicative 与 arrow 并支持处理器复用。
函数响应式系统的运行时验证与确认
利用纯函数式FRP的引用透明性，为跨平台响应式系统提供断言、记录回放与随机测试结合的运行时验证调试方法。
Leibniz 相等性与 Martin-Löf 同一性在参数性下同构
在函数外延性与参数性假设下，证明 Leibniz 相等与 Martin-Löf 同一性之间的互转构成同构。
更多前驱函数：一次表示法训练
从丘奇数与Kleene表示出发，系统推导出更小、更快、更精确的前驱函数表示。
依赖（余）模式匹配的加工：不遗漏任何模式
提出将依赖（余）模式匹配定义加工为核心语言 case tree 的算法，证明其保持首匹配语义并改进 Agda 实现。
类型化的 dataspace actor
为 dataspace actor 模型提出首个结构化类型系统，用类型接口防止错误数据传播并保障失败隔离。
基于广义续延的效应处理器
为深度、浅层和参数化效应处理器提出基于广义续延的 CPS 变换与 CEK 抽象机实现。
弹性表定义函数：将电子表格函数泛化到可变大小的输入数组
提出弹性表定义函数，将用户写定的定长数组函数自动泛化为可处理任意长度输入，并证明得到主泛化。
局部代数效应理论
提出类型系统追踪程序局部观察到的代数效应方程，避免全局平凡理论，支持可靠灵活的推理与优化。
Garsia–Wachs 算法的最优纯函数式实现
给出 Garsia–Wachs 算法的纯函数式实现，在保持最优叶树构造的同时达到 O(n log n) 时间。
更快的协程管道：一种重构
通过消除 connect 操作的互递归，从规约推导出三续延编码，并推广至双向管道，在基准测试中媲美主流 Haskell 流处理库。
评 Richard Bird 与 Jeremy Gibbons 的《Algorithm Design with Haskell》（Cambridge University Press, 2020）
书评：Bird 与 Gibbons 将算法视为从函数式规约出发、可用 Haskell 系统推导的计算对象。
评 John David Stone《函数式编程算法》（Springer-Verlag，2018）
评述一本以 Scheme/R7RS 讲授函数式算法与数据结构的教材，指出其抽象层次高但回避效率分析。
201915 篇 · vol.29
构造性 Galois 连接
提出构造性 Galois 连接，使抽象解释中的 Galois 连接可在依赖类型证明助手中机械化并支持可提取算法。
POPLMark 重装上阵：通过逻辑关系机械化证明
提出用Kripke式逻辑关系证明强规范化的基准，比较Beluga、Coq、Agda等证明助手对机械化元理论的支持。
如何用二阶计算分析器 SOL 证明等式理论的可判定性
提出二阶代数理论下证明等式理论可判定性的通用方法，并实现 Haskell 分析器 SOL。
纯同构类型系统（Pure Iso-Type Systems）
提出 PITS 演算族：以统一语法兼顾项与类型、支持无限制一般递归，并通过 iso-types 与显式 cast 保持类型检查可判定。
经验证的 CakeML 编译器后端
介绍经 HOL4 机器验证的 CakeML 编译器后端设计、12 个中间语言、语义证明与自举。
如何评估渐进类型系统的性能
提出首个评估健全渐进类型系统性能的方法，可量化绝对性能及同一系统不同实现的相对性能。
高阶函数前向自动微分中的扰动混淆
揭示高阶函数前向自动微分中扰动标记失效导致结果错误的微妙 bug，并讨论两种修复方案及其缺陷。
面向客户端–服务器模型的 RPC 演算理论
提出有状态 RPC 演算与位置类型系统，在编程视角支持对称通信、实现采用非对称通信，并统一三种服务器策略。
COCHIS：稳定且连贯的隐式机制
提出 COCHIS 演算，在保持类型安全、连贯性与类型替换稳定性的同时支持多态、局部作用域、重叠实例与高阶规则。
用 500 行代码实现的 SQL 到 C 编译器
用 500 行 Scala 将 SQL 关系代数解释器通过 LMS 与 Futamura 第一投影编译为高性能 C 代码。
全规约 Krivine 抽象机 KN 以锁步方式模拟纯正常序规约：基于对应演算的证明
证明改进的全规约 Krivine 抽象机 KN 以锁步方式模拟纯 λ 演算的标准正常序规约。
新兴语言：编程语言教学的一种替代方法
提出以新兴编程语言组织编程语言课程，替代按语言原理结构的传统教法，并论证其课程优势。
Peano 数上的左折叠与右折叠
从 Peano 数上的左、右折叠出发，用幂集等标准函数展示折叠模式的定义与推导。
评《The Haskell School of Music：从信号到交响曲》
评述《The Haskell School of Music》，介绍其用 Haskell 与 Euterpea 统一音乐符号表示、演奏控制与音频合成的教学路径。
如何找到假币
给出在 n 枚硬币中用天平以最少保证称量次数找出可能存在的假币并判定其轻重的方案。
201821 篇 · vol.28
抽象分配：控制流分析中 polyvariance 的统一方法
提出可调抽象分配函数，统一并泛化高阶控制流分析中的 polyvariance，且保证可靠性。
从零构建 Iris：高阶并发分离逻辑的模块化基础
以第一性原理统一、完整地阐述 Iris 3.1 的设计与语义基础，为高阶并发分离逻辑奠定模块化框架。
证明相关的合一：仅使用你的类型论公理的依赖模式匹配
提出证明相关的合一框架，使合一规则只依赖所在类型论自身的公理，并据此重写 Agda 的合一算法修复大量缺陷。
类型错误的系统性识别与传达
提出 counter-factual typing 与 variational typing，系统定位类型错误、生成纠错信息并排序呈现最可能原因。
依赖互操作性的基础
用类型论部分 Galois 连接与反连接为依赖互操作性建立语义基础，并在 Coq 中机器验证。
计算经典逻辑与相继式演算教程
通过相继式演算的计算解释，以对偶性统一控制流、求值顺序、严格/惰性语言及聚焦与类型安全。
1ML —— 核心与模块的统一
提出 1ML，将 ML 核心与模块统一为一种语言，使模块成为一等值，并用 System Fω 表达其类型结构。
应用式双向编程
提出应用式高阶双向编程框架，让双向变换能以标准函数式语言中的单向程序编写，并桥接 lens 与语义双向化两种方法。
Launchbury 惰性求值自然语义的 adequacy
在 Isabelle 中机器验证 Launchbury 惰性求值自然语义的 adequacy，首次给出严格证明。
基于 size 的高阶重写终止性
提出基于类型/大小分析的通用模块化准则，用于证明扩展用户重写规则的单型 λ 演算终止。
将契约监控策略视为通信模式的扩展论述
将契约检查统一重构为并发进程间通信，并在核心演算中嵌入多种监控策略及证明其正确性。
静态类型错误的动态见证（或：类型不正确的程序通常确实会出错）
提出为静态类型错误合成反例见证输入，证明病态程序通常会出错，并用归约图和用户研究辅助调试。
Ghostbuster：简化并转换 GADT 的工具
提出 Ghostbuster，可省略选定类型参数来生成简化 GADT，并自动生成类型安全的往返转换函数。
查询引擎中的推式与拉式循环融合
系统比较推式与拉式查询引擎，揭示其与循环融合的联系，提出融合二者优点的新型拉式引擎。
基于 lineage 的分布式计算：编程模型与基础
提出 function passing 编程模型与类型化核心演算，为基于 lineage 的分布式计算奠定基础并简化容错。
Batcher 奇偶归并网络揭秘
以函数式珍珠形式深入剖析比较网络理论，揭示 Batcher 奇偶归并网络的结构。
Parberry 成对排序网络揭秘
用比较网络的单调性重新解释 Parberry 成对排序网络，并厘清其与 Batcher 归并交换网络的关系。
大数据编程语言专刊编辑导言
介绍大数据编程语言专刊，指出编程语言思想正推动以数据为中心的计算研究，并征集成熟成果。
并行与并发函数式编程专刊社论
介绍《函数式编程杂志》并行与并发函数式编程专刊，展示函数式语言与概念在该领域的现状与应用。
在基于 HtDP 的 CS1 课程中通过函数式视频游戏融入分布式编程
提出用函数式多玩家分布式视频游戏设计配方，将分布式编程引入 HtDP 式 CS1 课程。
论 2-3 树的构造
讨论自顶向下、自底向上和增量式三种线性时间构造 2-3 树的方法，其中增量式可与其他操作交错。
201722 篇 · vol.27
面向忙碌程序员的 QuickSpec 快速规范
提出 QuickSpec 的新理论探索架构，通过测试 Haskell 程序自动发现更复杂、更快的等式性质与引理。
函数式科学工作流语言 Cuneiform 的计算语义
给出 Cuneiform 的抽象语法、简单类型系统与求值语义，并提供 Erlang 参考实现。
面向 CIC 的新合一器可理解指南：包含宇宙多态与重载
完整描述并实现支持宇宙多态与重载（规范结构）的 CIC 合一算法，并在大型库上验证启发式足够。
公平枚举组合子
提出枚举组合子的公平性理论，设计公平组合子并证明其性质，用于属性测试更高效地发现程序语言模型缺陷。
支持异常的灵活动态信息流控制
提出 LIO：以 Haskell 库形式实现动态信息流控制，用浮动标签与 current clearance 处理异常下的机密性与完整性。
作为幺半群的计算概念
把 monad、applicative functor 和 arrow 统一为 monoidal 范畴中的幺半群，并给出自由幺半群与 Cayley 表示及关系分析。
面向分布式大数据分析的代数
提出基于幺半群同态的代数，作为 MRQL 形式基础，统一数据密集型分布式计算 DSL 操作并支持查询优化。
依赖 lambda 消去演算
提出 CDLE：仅用纯 lambda 编码、无需辅助数据类型系统的依赖类型演算，并证明其逻辑一致性。
代数效应与处理器不需要值限制
提出可对任意计算泛化的 HM 多态类型系统，证明代数效应与处理器的可靠性，无需值限制。
政策建议与可避免性的计算理论贡献
用依赖类型构造性地形式化政策建议、生存性、可达性与可避免性，并研究其可判定条件与通用评估过程。
Ornaments 的本质
用多类签名抽象索引数据类型，为 ornaments 建立去语法化模型，使其可推广到 GADTs/refinement types。
Agda 中的交互式编程——对象与图形用户界面
提出 Agda 中基于共归纳 IO 与 copattern 匹配的交互式对象编程方法，实现 ooAgda 库并支持 GUI 与对象验证。
编译的五十年历程
以等式推理从正确性规约直接推导出算术表达式编译器，重访编译器验证的起源。
模块化高阶基数分析：理论与实践
提出一种模块化高阶基数分析，可识别单次使用的 thunk 与 lambda，并证明其相对 call-by-need 语义的可靠性。
正规序归约文法
提出为给定 n 生成无歧义正则树文法，刻画恰需 n 步正规序归约的 SK 组合子项。
有限性与有理序列：构造性方法
在Martin–Löf类型论中构造性地实现有理序列，证明两种有限性概念可互换，并引入带回溯指针的列表。
基于能力的分布式异构查询本地化
提出数据操作语言和类型导向的查询本地化机制，通过能力感知重写将分布式异构查询编译为原生查询。
依赖类型编程专刊导言
本期特刊导言回顾依赖类型编程的基础与发展，并介绍收录的六篇覆盖广泛主题的论文。
代数数据集成
提出基于多排序等式代数理论与伴随迁移函子的数据集成框架，并实现查询语言 AQL。
通过分配律与左零幺半群实现带 cut 的回溯
用代数效应为列表单子加入 Prolog 的 cut，并给出自由左零幺半群与分配律复合两种单子刻画。
Call-by-name 外延性与合流
在 sequent calculus 中为带效应的 call-by-name 惰性外延函数给出合流规约系统，并揭示其边界。
博士论文摘要
汇总上一年度完成的函数式编程博士论文摘要，作为面向社区的学术服务。