LMCS（共 1020 篇）
Logical Methods in Computer Science，开放获取
202681 篇 · vol.Volume 22, Issue 2
基于神经网络的定量验证
用神经网络表示上鞅证书，通过反例引导的归纳合成循环，为概率程序与随机模型计算紧致且可靠的概率界。
面向 PRISM 的概率编排语言
提出一种概率编排语言，定义概率语义并编码到 PRISM，支持并发概率系统的全局建模与模型检测。
FBFL：一种面向联邦学习中数据异构性的基于场的协调方法
提出FBFL，以场协调和宏编程实现分布式选举与自组织分层联邦学习，缓解non-IID并提升鲁棒性。
面向 UNSAT 的基于归结的交互式证明系统
将竞争性交互证明归约为算术化问题，并给出首个与 Davis-Putnam 归结竞争的 UNSAT 交互协议。
时序数字电路的完备理论：指称、操作与代数语义
为时序数字电路建立指称、操作与代数三种可靠且完备的语义，并给出观察等价与范式代数理论。
最优重写公式与数据库查询：项重写、结构分解与复杂度的交汇
该论文为正向一阶公式在常见等价保持重写规则下的宽度最小化给出完备算法，连接项重写、查询求值与结构分解。
基于双蕴含点的扩展归结子句学习
提出基于双蕴含点的扩展归结子句学习算法，在CDCL SAT求解器中动态引入新变量，提升Tseitin与XOR类公式求解性能。
在立方类型论中自动化边界填充
提出面向立方类型论的边界填充自动化方法，统一求解 contortion 与 Kan 问题，并实现 Haskell 求解器。
机器空间 I：弱指数与紧空间上的量化
引入机器空间区分可验证性质与其验证过程，构造弱指数，并给出紧空间上全称量化的拓扑算法。
在分离逻辑的极小片段中编码 Peano 算术
将 Peano 算术 Π⁰₁ 公式编码到仅含直觉 points-to、0 与后继的分离逻辑片段，证明有效性等价与不可判定。
使用序列网络的度量时序逻辑在线监控
提出“未来时序标记”技术，从 MTL 规约统一构造序列网络，实现离散与稠密时间下的高效在线监控。
深入与拓宽：有界树深与树宽图上的计数逻辑与同态不可区分性
重新证明并拓展计数逻辑与同态不可区分性关系，分离有界树宽/树深类，并证明相关图类同态区分封闭。
时间不透明性的光明面
通过限制系统、攻击者及观测次数，证明时间自动机不透明性在多个子类与新定义下可判定。
二阶 HyperLTL 的复杂度
确定了二阶 HyperLTL 可满足性、有限状态可满足性与模型检测的复杂度，并分析两个受限片段及闭世界语义。
协议分析中的知识问题：扩展子项收敛（subterm convergent）的概念
提出图嵌入项重写系统及收缩收敛子类，证明后者的协议知识问题可判定、前者不可判定，并给出组合结果。
模 traced comonoid 结构的重写
将弦图超图重写推广到 traced comonoid 范畴，建立完全性并适配 DPO 重写，附顺序电路案例。
下推多智能体系统的模块检查
确定了下推多智能体系统对 ATL 与 ATL* 的模块检查复杂度，分别为 2EXPTIME 完全与 4EXPTIME 完全。
succinct 图上的一元二阶公式硬度
证明 succinct 图上 cw-nontrivial MSO 性质为 NP-hard 或 coNP-hard。
面向 Graph API 的污点分析：聚焦访问控制失效
提出首个针对 Graph API 的静态与动态污点分析系统方法，用图变换与临界对分析系统性检测访问控制失效。
PRAM 上工作高效的常数时间查询求值
在 CRCW PRAM 上为关系代数、无环查询、半连接代数和最坏情况最优连接查询给出常数时间且弱工作高效的求值算法。
基于广义加权类型图的图变换系统终止性
改进并推广加权类型图方法，证明更广的DPO图变换系统及变体的终止性。
用 Uppaal 对契约自动机运行时环境的形式化分析：建模、验证与测试
用 Uppaal 对 CARE 中间件做随机时间自动机建模、穷尽与统计模型检测，并自动生成具体测试用例。
有限时域概率并发博弈系统中的均衡验证
证明子博弈完美均衡验证在 PSPACE，而 Nash 均衡验证为 EXPTIME-完全，揭示反直觉复杂度差异。
条件重写模（conditional rewriting modulo）的合流性
为条件重写模 E 提出基于条件临界对的合流性证明与反证方法。
JustAct：受组织间策略监管的可审计多智能体系统框架
提出 JustAct 框架，刻画由组织间策略监管且可审计的多智能体系统，并证明行动许可决策不可被后续信息推翻。
卵石游戏与代数证明系统
建立卵石游戏与代数证明系统 NS/MC/PC 的对应，导出度数分离与度数-规模权衡。
匹配命令式算法时间复杂度的基于规则的图程序
通过改进 GP 2 编译器的图数据结构，使基于规则的图程序在任意节点度图上达到命令式算法的时间复杂度。
可同步邮箱通信的一种基于自动机的方法
提出自动机方法，证明无轮大小限制的邮箱通信系统可同步性判定是 Pspace 完全。
公平资源交换的策略
提出策略语言MuAC与逻辑MuACL，将资源交换公平性归约为逻辑证明并证明可判定。
高效计算无歧义有限自动机秩的谱方法与组合方法
证明计算无歧义有限自动机对应零一矩阵幺半群最小秩属于 NC，并给出 O(mn^4) 时间算法及弱 Černý 型结果。
通过可表达性刻画合取线性代数查询的枚举与更新
界定 MATLANG 中与 free-connex、q-hierarchical 合取查询对应的片段，识别支持常数延迟枚举和常数时间更新的线性代数程序。
面向嵌套图条件的局部化 RETE 增量图查询
提出局部化 RETE，使图查询可在相关子图上局部增量执行并保持结果完备。
无限与有限迹上 LTL 性质的异步组合
提出面向异步数据端口组件的 LTL 重写方法，将局部性质转为全局性质以支持组合式验证。
在按值调用中表示守卫性与守卫参数化单子
论文将按值调用的守卫迭代语义推广到参数化单子，把守卫性刻画为程序内在的范畴性质。
全称量化使自动结构难以判定
证明自动结构中消除单个全称量词会导致 NFA 双重指数爆炸，且判定空性为 EXPSPACE 完全。
论一阶理论中 k-否定片段的多项式时间可判定性
提出一个通用框架，给出固定否定符号数的一阶理论片段多项式时间可判定的充分条件，并应用于弱 Presburger 算术等理论。
利用窗口计数约束在反应式系统合成中减少状态空间爆炸
提出窗口计数约束与迭代合成，利用获胜区域缩减自动机，缓解反应式系统合成的状态空间爆炸。
一个足矣：不含一阶变量的二阶合一
提出仅含一个二阶变量且无一阶变量的 SOGU 片段，并证明其结合变体 ASOGU 不可判定。
AuDaLa 的表达能力：图灵完备性与可能的扩展
通过在 AuDaLa 中实现并验证图灵机，证明其图灵完备，并探讨提升实用表达力的扩展。
有界参数化时间自动机的稠密整数完备综合
提出有界参数化时间自动机的参数综合算法，能终止并给出稠密下近似，包含整数点及其凸组合。
确定性后缀读取自动机
提出确定性后缀读取自动机 DSA，研究其最小化问题，并证明寻找最小等价 DSA 是 NP 完全问题。
带聚合的合取查询答案的直接访问
研究带分组聚合的合取查询在注解数据库上的细粒度复杂度，给出答案字典序直接访问的易处理条件。
带否定的合取查询的直接访问
将合取查询直接访问的可处理性结果推广到含负原子的情形，并用电路表示答案集。
范畴概率中的经验测度与强大数定律
用准马尔可夫范畴公理化经验采样态射，联合证明 de Finetti、Glivenko–Cantelli 与强大数定律。
多面体模型检测中的弱单纯形互模拟与最小化
提出多面体模型上的弱单纯形互模拟与胞腔偏序模型上的弱±互模拟，并给出基于LTS编码和mCRL2的最小化方法。
统一分级线性逻辑与微分算子
将分级线性逻辑与微分线性逻辑统一，用微分算子幺半群索引指数连接词，并给出基于分布论的指称模型。
有界路径宽度上的一阶逻辑再探
证明有界路径宽度图上的 FO 性质可在线性时间判定，且对公式依赖为初等，推广有界树深元定理。
博弈、移动进程与函数——交替、并发与良括号语义
建立 λ-演算的 π-演算编码与操作博弈语义的紧密联系，证明二者诱导的等价一致并迁移多项结果。
单值富集范畴与富集 Rezk 完备化
证明单值富集范畴间本质满且完全忠实的函子是等价，并构造富集 Rezk 完备化及单值富集 Kleisli 范畴。
论 NP ∩ coNP 证明复杂度生成器
提出由证明系统定义的 Σ₂ᵖ 搜索问题 DD_P 与假设 (ST)，并在模型论假设下证明它蕴含 NP≠coNP。
镜像 call-by-need：或值表现得愚蠢
提出 call-by-silly 退化演算，镜像 call-by-need，合并按名重复与按值擦除的最差行为，并用多类型与抽象机分析。
MSO 中序数秩的二分定理
证明全二叉树上 MSO 公式的良基见证序数秩要么小于 ω²，要么达到 ω₁，且可判定属于哪种情形。
因果图动力学与 Kan 扩张
证明因果图动力学可表达为 Kan 扩张，并揭示单调子类及其普遍性。
Σ_0^2 中的位置性与一个完备性结果
刻画 Σ_0^2 中具有位置策略且含中性字母的目标，并证明平均收益的位置性及完备性结果。
同伦类型论中的终结余代数与非良基集合
在同伦类型论中构造满足 SAFA 与 AFA 的非良基集合模型，并推广反基础公理与 M-类型 identity type 刻划。
关系范畴的分类体系
系统梳理抽象关系结构性质的各类范畴，并揭示其作为对称幺半单子 Kleisli 范畴的统一来源。
利用最弱应用条件对图变换进行排序以支持图修复
提出损伤/修复指示应用条件，用最弱条件刻画图变换的修复增益并排序以修复不一致图。
从 codereliction 导出加法富集
证明 codereliction 即使定义在非加法环境中也会通过双代数卷积诱导加法富集，并刻画微分线性范畴和唯一性。
同伦类型论作为 ∞-logos 图的语言
用带 lex 可及模态的 HoTT 重建 ∞-logos 图，并给出高维 synthetic Tait computability。
多模态类型论的规范化
证明了多模态类型论 MTT 的规范化，并将类型检查与转换判定归约为底层模态相等性，从而给出统一算法。
PV₁ 模型中的素因子分解
在特定密码学困难性假设下，PV₁ 即使加入 BB(Σ^b_0) 也不能证明每个数有素因子，并由此得到非标准模型。
简单类型常域模态 λ 演算 I：距离化 β-归约与组合逻辑
提出参数化模态简单类型 λ 演算 λθ，给出基于 BCKW 组合逻辑的模型刻画及与最大系统 λω 的保守性结果。
循环、逆极限与非确定性
引入 Weihrauch 复杂度中的无限循环/逆极限算子，证明其单调性并刻画非确定性可计算问题的封闭性。
自动结构的简单类
研究多项式增长自动结构与Presburger结构两类子类，刻画其中群和等价结构的代数性质。
求解折扣支付博弈的一种目标改进方法
提出一种完全对称的目标改进算法，通过约束系统与误差最小化求解折扣支付博弈。
无限树的扩张问题
研究无限树的 Ramsey 型定理等组合工具，并应用于树代数的扩张问题。
一元二阶可定义上下文无关图集合的刻画
给出 CMSO 可定义且上下文无关图语言的三种等价刻画，并连接树到图可定义转换与可定义树分解。
半可计算图的可计算逼近
证明可计算度量空间中的半可计算图均可由端点可计算的子图任意精度逼近。
守卫 TGDs 查询应答的更紧界
通过区分守卫原子与侧签名的元数，改进守卫 TGDs 开放世界查询应答的复杂度上界。
面向（非确定性）分支程序系统的证明者-对手博弈
为确定性与非确定性分支程序上的证明系统 eLDT/eLNDT 引入 Pudlák-Buss 型证明者-对手博弈，并证明二者多项式等价。
认知技能：关于知识与遗忘的推理
提出加权模型上的认知逻辑，以“认知技能”刻画知识获取与遗忘，并研究可认知性、可遗忘性及计算复杂度。
纤维范畴的 Hofmann–Streicher 提升
将 Hofmann–Streicher 宇宙提升推广为相对版本，并以伪伴随和 2-双纤维化重新刻画。
新皮尔士关系演算
用图表式幺半语法替代笛卡尔语法，提出与一阶逻辑等表达力的新皮尔士关系演算，并给出完全公理化。
显式化的无穷递降计算
提出显式标注序数变量的非良基证明系统，证明有效证明可计算，并导出规范化与范畴模型。
可见下推语言的 AC^0 复杂度
给出判定可见下推语言是否在 AC^0 中或 ACC^0(m)-难的算法，并引入中间 VPL 子类。
模态逻辑中不动点公式的可定义性与可分离性复杂度
系统刻画模态不动点公式可分离性与可定义性在不同模型类上的计算复杂度，并给出分离子构造算法。
剩余格结构中的局部性
研究经典 Hanf 与 Gaifman 局部性定理在剩余格多值模型中的推广与失效条件，并借助序解释连接词恢复主引理。
约束满足问题、紧致性与不可测集
证明宽度为一的有限关系结构在 ZF 中紧致，否则其紧致性蕴含 3 维空间存在不可测集。
一种可扩展的博弈论方法：从标准化目录中选择安全控制
提出基于两人零和博弈与代数依赖建模的安全控制组合选择方法，并在ITSG-33目录上验证可扩展性。
LMCS vol.Volume 22, Issue 42026
保守 Petri 网的结构活性
证明保守 Petri 网的结构活性是 EXPSPACE 完全的，并给出最小活标识的双指数上界。
2025122 篇 · vol.Volume 21, Issue 2
异步多方会话类型中的崩溃停止故障
提出带崩溃停止故障的异步多方会话类型理论，借助崩溃处理分支与全局语义，证明良类型进程在崩溃下仍保证无死锁与活性。
FlexFringe：通过学习概率自动机建模软件行为
FlexFringe 提供高效的概率确定性有限自动机学习实现，可从软件日志学习可解释模型并用于异常检测。
正则模型检测倒置：一种基于不变式的方法
提出基于不变式的自顶向下正则模型检测，用 b-不变式将可达集逼近为正规集并构造自动机验证安全性。
定量性质与自动机的安全性和活性
将布尔安全-活性分类推广到定量性质，并为常见定量自动机给出安全/活性判定、安全闭包与分解。
锥上的积分
为可测锥建立积分理论，使概率编程语言的抽样原语可在锥语义模型中获得解释，并构造线性逻辑的两个指数余单子。
模群（Groups）的同余闭包
提出模群公理的同余闭包框架，通过等式完成过程构造基收敛重写系统，并在终止时判定相关字问题。
FMplex：探索 Fourier-Motzkin 与单纯形法之间的桥梁
提出 FMplex，用量词消去处理线性实数算术合取，通过分支将最坏复杂度从双指数降至单指数。
死锁避免的分布式控制器合成
提出两种限制使带锁系统的分布式死锁避免控制器合成可判定，并刻画其精确复杂度。
混合归纳与余归纳类型的 size-change 原理
将 size-change 原理推广为 totality 检查，以在混合归纳与余归纳类型下可靠验证递归定义。
区间与集合方法在控制与状态估计中的离线与在线使用：若干方法论途径及其应用
综述区间与集合方法在控制与状态估计中的离线分析与在线实现，并回顾多类实际应用。
结构约简与 stutter 敏感性质
提出 shortening/lengthening 不敏感语言以推广 stutter 不敏感，并给出基于结构约简的半判定验证。
Ariadne 中的严格函数演算
介绍 Ariadne 框架及其严格函数演算，支持欧氏函数模型、方程求解与混合系统分析。
TSO 博弈——总存储序语义下安全博弈的可判定性（含附录的扩展 LMCS 版本）
将 TSO 语义扩展为回合制双人安全博弈，并给出不同缓冲区刷新责任下可判定性的完整图谱。
SLP 压缩文档的常数延迟枚举
提出在 SLP 压缩文档上对 annotated automata 查询进行结果枚举的算法，实现 output-linear/常数延迟并改进已有对数延迟。
树上的 MSO 查询：利用森林代数在更新下枚举答案
提出对数高度森林代数表示框架，实现树上 MSO 查询在局部更新下的高效答案枚举。
HyperLTL 可满足性是高度不可判定的，HyperCTL* 则更难
确定 HyperLTL 与 HyperCTL* 可满足性的精确复杂度：分别为 Σ₁¹-完备与 Σ₁²-完备。
Chomsky-Schützenberger 表示定理的范畴轮廓
用纤维化与 operad 范畴方法统一广义 CFG/NFA，并推广 Chomsky-Schützenberger 表示定理。
多世界演算
提出彩色 PROP 演算统一配对与选择，参数化经典、概率、非确定与量子分支，并证明通用性与等式完备性。
带传递闭包的正关系演算的图上导数
证明 PCoR* 及其测试/名义扩展的等式理论复杂度，并用图上导数构造自动机进行判定。
具有任意权重的单时钟加权时间博弈的可判定性
证明允许任意权重（含负权）的单时钟加权时间博弈可判定，并可在指数时间内计算值函数。
可计算泛函理论 TCF 中的强否定
在可计算泛函理论 TCF 中定义公式与谓词的强否定，并证明其关键逻辑性质与构造性数学适用性。
多折扣因子的折扣和自动机
定义带多个整数折扣因子的非确定折扣和自动机，揭示其不可判定性，并提出整洁子类恢复良好性质。
学习一阶计数逻辑（FOCN）中可定义的概念
将一阶逻辑可定义分类器的亚线性学习推广到带计数一阶逻辑 FOCN，并证明无界度下不可亚线性学习。
可判定一阶片段的 Craig 插值
证明 guarded-negation 片段是 guarded 片段保持 Craig 插值的最小扩张，并给出其他片段插值扩张的不可判定性。
会话编程中基于检查点的回滚恢复
提出支持提交、回滚与中止原语的会话语言，用类型级可判定合规性检查静态防止越界回滚，并证明无错误性与进展。
可逆系统的非干扰分析：一种基于分支双相似性的方法
提出基于分支双相似性的非干扰性质分类，揭示可逆计算中弱双相似性无法捕获的隐蔽信息流。
棋子博弈
引入棋子博弈，其中顶点控制权通过棋子归属动态变化，并刻画可达性目标的求解复杂度。
概率图上的查询近似
系统刻画概率图上查询求值何时存在组合 FPRAS，并给出可近似与（条件）不可近似结果。
单值基础下的单子形式理论
在单值基础中形式化 Street 的单子理论，构造内蕴单子双范畴并证明其单值性，全部结果由 Coq/UniMath 机器验证。
合取正则路径查询的语义树宽与路径宽
证明对任意 k，判定 UC2RPQ 是否等价于树宽 k 的查询可判定，并给出最大下近似与复杂度。
论准离散闭包空间上的互模拟
为准离散闭包空间提出三种互模拟，并给出对应的空间模态逻辑刻画及与已知等价的联系。
检验量子连续时间马尔可夫链上的连续随机逻辑（CSL）
提出投影、矩阵指数与定积分结合的代数方法，判定并高效模型检测量子CTMC上的CSL公式。
二阶多项式时间（second-order polytime）的完备且可处理的机器无关刻画
首次给出 BFF（二阶多项式时间泛函）的多项式时间可判定、可靠完备且隐含的刻画。
前幺半范畴的弦图
证明带 runtime object 的弦图是 effectful 范畴的内部语言，并可用于前幺半、Freyd 等范畴。
输出位于任意幺半群的确定性转换器的主动学习
利用范畴框架研究输出在任意幺半群中的确定性转换器，给出其最小形式存在唯一条件，并导出基于成员与等价查询的主动学习算法。
策略作为资源项及其范畴语义
通过 augmentation 直接建立正规资源项与 Hyland-Ong 策略的对应，并给出归约不变的指称模型与资源范畴。
通过高阶重写与元组解释刻画基本可行泛函
本文证明由多项式有界代价-尺寸解释的高阶项所表示的泛函类恰好是类型二基本可行泛函类 BFF2。
面向 some 与 all 的对齐完备关系 Hoare 逻辑
证明一般对齐自动机下 ∀∀ 与 ∀∃ 关系 Hoare 逻辑的对齐完备与 Cook 完备性。
从最内层到完全概率项重写：几乎必然终止、复杂度与模块性
将最内层重写的终止与复杂度准则推广到概率项重写，证明几乎必然终止和复杂度可模块化分析。
均匀一维片段中的交替量词：兼探三变量逻辑
研究均匀一维片段中块内交替量词的可满足性，证明两类限制具有有限模型性质且为 NExpTime 完全。
一种鲁棒的基于图的观察等价性方法
提出基于局部推理与图邻域的鲁棒性条件，逐步证明观察等价性，并推广到受限上下文与归约步数。
随机窗口平均收益博弈
研究随机二人博弈中窗口平均收益目标的策略求解，给出复杂度界，并归约到非随机博弈。
超越奇偶博弈中的值迭代：通用树上的策略迭代
为奇偶博弈提出通用树上的策略迭代框架，绕过值迭代需探索大量树节点的障碍，并实现每轮高效更新。
对抗观察者的隐私保护合成
研究在信号隐藏预算下，自动合成既满足规范又能对观察者隐藏秘密的反应式系统，并给出复杂度与认证方法。
半环上加权自动机学习的可行性
界定了 Angluin 式查询学习加权自动机在半环上的理论边界与可猜测函数类。
终止项重写系统上的小项可达性及相关问题
研究终止项重写系统中大小受限可达项的判定复杂度，并分析终止性证明方式与合流性的影响。
带交换（余）幺半群结构的对称幺半范畴的重写
为带交换（余）幺半群结构的 string diagrams 重写给出基于超图双推出重写的可靠完备刻画。
论对延迟具有鲁棒性的反应式策略的存在性
比较延迟控制博弈与延迟博弈，建立确定必胜策略的互归约，并揭示随机与概率获胜下的分离。
借助朋友的帮助：通过 Joker 动作的半合作博弈
提出 Joker 博弈，将并发博弈中的有限帮助建模为带成本动作，研究最小化 Joker 使用的策略，并用于模型测试生成。
通过有限宽度反模型判定一阶理论查询的可判定性
提出基于反模型宽度（含 partitionwidth）的通用框架，统一证明广泛逻辑蕴含/查询问题的可判定性。
从正则行为生成的分形
把 Milner 的进程表达式重新解释为完备度量空间上的收缩算子，从而给出分形等价的可判定公理化。
超时异步会话类型：面向定时交互的安全异步混合选择
提出 TOAST，用时间约束安全支持异步混合选择，从而在会话类型中建模超时并保证进展。
连续时间上的 Church 合成问题
将 Church 合成问题从离散时间推广到非负实数连续时间，并揭示其与离散情形的本质差异。
开放线性系统的范畴论处理
以范畴论和 copartiality 形式化开放随机系统，并统一扩展高斯分布与线性关系。
用于分支互模拟的正 Hennessy-Milner 逻辑
引入正模态逻辑与有向互模拟/分离，建立有向 Hennessy-Milner 定理并给出 HMLU 的正子逻辑 PHMLU。
数据感知的混合表列
提出面向带数据比较算子 XPath 的数据感知混合表列演算，证明其可靠、完备、终止，并确立可满足性为 PSpace 完全。
类型依赖的代数呈现
证明 C-系统与 B-系统范畴等价，解决 Voevodsky 猜想，并以 CE/E-系统统一二者。
论 M,N-粘合范畴的公理
把粘合范畴的刻画与 Grothendieck topos 嵌入定理推广到 M,N-粘合范畴，并引入 N-粘合态射。
带 AC 公理的左线性完成
为左线性项重写系统在 AC 公理下的完成过程给出新的正确性证明、模拟关系与典范性结果。
马尔可夫二项链的算法
形式化马尔可夫二项链，证明无环流几乎必然终止，给出近似与精确计算终止时间的算法，并编码至概率模型检测器。
离散时间网络与对称广播系统的参数化模型检测
研究离散时间参数化网络模型检测复杂度，无控制器安全为 PSPACE 完全、活性可 EXPTIME 判定，有控制器活性不可判定。
有限轨迹上的自动机线性动态逻辑
提出 ALDL_f，将命题逻辑与 NFA 结合，在有限轨迹上表达时序约束，可满足性属于 PSPACE，且表达力等价 MSO。
不动点检查的幺半范畴视角
从 gs-monoidal 范畴视角解释不动点检查技术，刻画其组合性并实现工具 UDEfix。
相对相干性的重写技术
扩展基于重写的相干性证明，覆盖部分相干与笛卡尔结构，并恢复单子/对称单子范畴相干定理。
利用不确定性查询不一致的描述逻辑知识库
提出利用概率语义 DISPONTE 查询不一致描述逻辑知识库，并在 TRILL/BUNDLE 中实现且与修复语义比较。
正则范畴中的 Aczel-Mendler 双模拟
将 Aczel-Mendler 双模拟推广到一般正则范畴与 topos，并在不依赖选择公理时证明其对复合封闭及一致性。
带一个 Mahlo 宇宙的 Martin-Löf 类型论中不可达集的解释
证明仅需一个 Mahlo 宇宙加可及性谓词，即可自底向上解释 CZF 的全部超限阶不可达集，并在 Agda 中形式化。
带不动点的（循环）证明系统的计算表达力
证明带最小/最大正不动点的 muLJ 与其循环扩展 CmuLJ 具有相同计算表达力，均对应 Π^1_2-CA_0 中可证全的函数。
多态效应演算中显式子类型强制转换的化简
提出多态效应演算中显式子类型强制转换的化简方法，消除编译开销并证明语义保持。
合取查询结果的排名枚举
提出带小预处理、对数延迟和可控空间的合取查询结果排名枚举算法，并给出必要性下界。
MacroSwarm：一种面向群体编程的基于场的组合式框架
提出基于场的组合式群体编程框架 MacroSwarm，用可复用纯函数块将感知场映射为动作目标场。
更新下带自由访问模式的合取查询
提出全动态求值方法支持所有带自由访问模式的合取查询，并刻画常数更新/延迟条件与复杂度权衡。
带投影的合取查询的枚举算法
提出带投影合取查询的枚举算法，通过交错预计算与连接处理，为星形和路径查询提供延迟保证并改进已知结果。
非确定性的层级
研究无限字上自动机非确定性的三层分级，证明其严格性并分析表达力、判定复杂度与概率刻画。
合取查询答案的多样性
研究合取查询及其扩展中，选取 k 个答案达到给定多样性水平 d 的判定与计算问题。
无限博弈中的记忆刻画
把位置策略的 universal graph 刻画推广到有限/无限记忆上界，并用 antichain 大小精确对应记忆量。
不平衡三角形检测与合取查询并的枚举困难性
将UCQ枚举的可处理性障碍归约到不平衡三角形检测，并给出两自连接自由CQ并的二分性。
有界歧义向量加法系统（VASS）的语言包含是可判定的
证明有界歧义 VASS 的语言包含可判定，并确立若干限制下等价问题的 Ackermann 完全性。
作业车间调度的分解策略与 multi-shot ASP 求解
提出面向作业车间调度的多种时间窗口分解策略与 multi-shot ASP 求解方法，在紧时限内显著提升调度质量。
主键约束下一致查询回答的一个简单算法
提出一个多项式时间膨胀不动点算法，用于主键约束下一致查询回答的必然性判定，并覆盖已知部分二分情形。
无限数据树上的约束自动机：从 CTL(Z)/CTL*(Z) 到判定过程
引入整数数据树约束自动机，证明非空性 ExpTime 完全，并判定 CTL(Z)/CTL*(Z) 可满足性。
在加权时间博弈中采用随机策略以模拟记忆
证明在发散加权时间博弈和无权加权博弈中，随机策略无需记忆即可达到与经典确定值相同的值。
判定一阶模态逻辑中插值式与定义的存在性
确定一阶模态逻辑中插值式与定义存在性在若干片段上的可判定性与复杂度。
幺半范畴中的余归纳流
将因果流函数推广至任意对称幺半范畴，提出幺半流与反馈范畴，为数据流编程提供余归纳范畴语义。
论直觉主义 S^1_2 中电路规模界的不可证明性
证明 IS^1_2 无法证明 SAT 的固定多项式 co-nondeterministic 电路下界，并给出对应上界不可证明性。
经由 Lipschitz doctrine 的子结构逻辑中的定量相等
用 Lipschitz doctrine 为含分级模态的子结构逻辑建立定量等式（距离）的可靠完备范畴语义。
可计算归约的范畴化
用 Lawvere 学说范畴化图灵、Medvedev、Muchnik、Weihrauch 归约，并统一为量词完备化。
论 MMSNP 的守卫扩展
研究 MMSNP 与三个超类之间的守卫扩展，证明 GMSNP 的二分可归约到单关系签名，并引入仍具二分性的守卫不等式 MMSNP。
使用 spooky pebbling 的经典与量子空间权衡
首次将 spooky pebble game 用于一般电路，证明量子空间上界与 PSPACE 完全性，并给出 SAT 求解器评估权衡。
Kleene 第二模型的完备化
将 Kleene 第二模型 K2 的弱嵌入性质推广到任意基数，并证明其推广具有强完备化。
可逆Petri网与可逆事件结构的范畴论关联
将因果网扩展以刻画非对称冲突，并范畴化可逆Petri网与可逆非对称事件结构的关系。
布尔基、公式大小与模态算子数量
证明模态逻辑T中消去双蕴涵会使公式指数增大，完备布尔基仅分两类；S5则与命题逻辑一致。
混合归纳与共归纳类型的全性
为混合归纳/共归纳类型全性检查器建立 parity game 语义，将正确值解释为获胜策略。
子基编号与形式包含关系关联的多表示
弱化 Spreen 编号基表示条件，统一多种表示，并用强/形式包含关系保证 Cauchy 一致与多表示兼容。
在 eXchange 演算中编程分布式集体进程
提出「分布式集体进程」抽象，在 XC 演算中形式化并在 FCPP 中实现，统一刻画簇形成与集体任务。
正分支程序的证明复杂度
提出正分支程序证明系统 eLNDT+，证明其在正序列上多项式模拟 eLNDT，并给出计数函数及鸽巢原理的多项式证明。
关于二变量序不变性的表达力与复杂度
证明二变量序不变 FO 的序不变性判定是 coNExpTime 完全的，并刻画其表达能力。
在粘合范畴中沿推导移动推导保持脊
证明了在粘合范畴的图变换中，沿推导移动推导会保持其脊（最小限制）。
带距离的抽取
证明多项、超几何与Polya抽取在Kantorovich距离下均为等距映射，并给出大瓮与大抽取量极限。
Hydra 之战与 AC 终止性
用带 AC 符号的重写系统忠实编码 Hercules 与 Hydra 之战，并证明其终止性。
将同伦等价与带计算公理的依赖类型理论中的保守性相关联
用同伦等价和带属性范畴语义，证明外延类型理论相对带计算公理类型理论的保守性。
Presburger 算术的广义多项式扩展的可判定性
证明特定形式的二次广义多项式扩展 Presburger 算术后该理论不可判定。
Monad 在多加几页时能做什么、不能做什么
系统研究 delay monad 与代数效应的组合，刻画哪些效应可分配，并用弱双模拟挽救部分不可行情形。
经由幺半伴随的扩展 Stone 对偶
用幺半伴随统一扩展 Stone/Priestley 对偶，并建立 residuation 代数与 profinite 序幺半群等新对偶。
范围（Rényi）熵查询与分区
研究几何范围查询下高效计算 Shannon/Rényi 熵的数据结构，给出条件下界、精确结构与近似结构。
论 NEXP 更强下界的一致性
将 Atserias 等人的方法推广，证明 NEXP ⊄ EXP/poly 与 NEXP ⊄ coNEXP 在更强有界算术理论中一致。
多结构博弈与量词数量
提出多结构博弈，以轮数精确刻画一阶句子的量词数量，并完全刻画区分不同大小线性序所需的最少量词数。
带一条新增转移的随机确定性自动机
证明在随机 DFA 上加入一条随机转移后，其语言的最小 DFA 期望规模可超过任意多项式。
Fresh-register 自动机中的互模拟
研究寄存器/新寄存器自动机互模拟复杂度：一般情形 EXPTIME 完全，无重复值情形为 PSPACE/NP，pushdown 扩展不可判定。
Z^2 的特殊仿射群中的 Identity Problem
证明 Z^2 特殊仿射群中有限生成子半群的 Identity Problem 与 Group Problem 均可判定且 NP-完全。
带弱恢复的分布式系统的行为理论
提出带崩溃恢复的分布式演算，并给出上下文等价的全抽象弱互模拟刻画。
Max-Plus 自动机的 Big-O 问题是可判定的（PSPACE-完全）
证明 Max-Plus 自动机的 Big-O（仿射支配）问题可判定，且复杂度为 PSPACE-完全。
线性可逆计算的 Curry-Howard 对应
提出线性可逆语言及其与 μMALL 的 Curry-Howard 对应，用原始递归生成满足有效性的循环证明并模拟切消。
基于扩展寻址机器的 PCF 完全抽象模型
证明 EAM 对 PCF 的模拟是终止等价的，并借助可类型化 EAM 与可定义性给出 PCF 的完全抽象模型。
外延与非外延的函数作为进程
在 Internal π 中以 wire 参数化细化 Milner 编码，刻画外延/非外延 λ-理论及其与 Böhm 树相等性的对应。
逻辑中组合方法的范畴论视角（扩展版）
用扩展的博弈余单子语义统一刻画 FVM 型定理，为有限模型论中的组合方法提供参数化范畴论基础。
从薄并发博弈到广义结构种（扩展版）
在薄并发博弈与广义结构种两类线性逻辑指称模型间建立形式桥梁，并用 double category 与 bicategory 刻画动态-静态对应。
论不含阿贝尔正规子群的群的描述复杂度
证明无阿贝尔正规子群的有限群可由 7 个 pebble、7 轮的 Hella 双射 pebble 博弈识别。
乘法-加法线性逻辑的类型同构
刻画乘法-加法线性逻辑（MALL）中的类型同构，给出含分配律与消去律的更丰富等式理论。
跳跃自动机的定量语义
为跳跃自动机提出四种基于跳转代价的定量语义，并确定其有界性问题的可判定性与复杂度。
论图类的一阶转导
系统研究图类的一阶转导拟序，证明局部范式，并揭示其非格性、路径宽度层级严格性及弱稀疏类作用。
不可分性与一致计算强度
用 Weihrauch 复杂度刻画有理数序与等价关系 ℰ 的不可分问题，并定位其计算强度。
202496 篇 · vol.Volume 20, Issue 1
证明作为有状态程序：带抽象 Hoare 三元组的一阶逻辑及其到命令式语言的解释
提出带抽象 Hoare 三元组的一阶逻辑，并用可实现性解释将证明抽取为有状态程序。
不动点方程系统上的操作
研究完备格上不动点方程系统在变量代入、方程重排等操作下解保持不变的条件，并提供机器检查证明。
精确实数计算的语义、规约逻辑与霍尔逻辑
提出精确实数计算语言 ERC，给出可计算完备的指称语义、可判定规约逻辑及可靠且表达力强的霍尔逻辑。
马尔可夫决策过程中概率提升因果性的基础
为 MDP 中基于概率提升的因果关系奠定数学基础，并分析其算法与复杂度。
历史确定性的时间自动机
证明历史确定性时间自动机严格介于确定性与非确定性之间，并使其 universality、inclusion 与 synthesis 判定为 EXPTIME 完全。
带测试与顶元素的 Kleene 代数的完备性定理
证明了带测试与顶元素的 Kleene 代数的两个完备性定理，并给出二元关系等式理论的 PSpace 算法。
形式化图变换的双推出（DPO）方法
在 Isabelle/HOL 中形式化双推出图变换基础理论，并机器验证推导唯一性与 Church-Rosser 定理。
分析噪声存在下 Angluin L* 算法的鲁棒性
实验分析 Angluin L* 的噪声鲁棒性：随机噪声下表现良好、结构化噪声下较差，并证明随机过程几乎必然产生非递归可枚举语言。
定量效应的和与张量
把代数效应的和与张量组合推广到定量代数效应，证明其分别对应 monad 的余积与张量，并给出应用。
为 ω-正则语言接受器构造简洁的特征样本
证明非确定性 ω-自动机无多项式规模特征样本，并为完全信息化的确定性 ω-自动机给出多项式时间构造与学习算法。
连续 Petri 网中的分离器
证明连续 Petri 网的不可达性可由多项式时间可构造的局部闭分离器见证，并可在 NC 内验证该证书。
Zeta 函数与马尔可夫过程的（线性）逻辑
揭示 Zeta 函数与程序执行的 cocycle 联系，并为 sub-Markov 过程建立二阶线性逻辑模型。
通过宇宙多态精化与直谓理论共享证明
提出宇宙多态精化方法，将非本质非直谓的证明翻译到直谓证明助手，并实现 Predicativize 工具。
非单调资源度量下并发程序的最坏情况输入生成
首个面向并发程序、在内存等非单调资源度量下可靠的（相对完备的）最坏情况输入生成算法，结合资源标注会话类型与符号执行。
Sturmian 词的可判定性
证明在 Presburger 算术上加入单个 Sturmian 词的一阶理论可判定，并实现 Pecan 自动证明相关定理。
事件时钟自动机的模拟
提出基于模拟的 zone 算法求解事件时钟自动机可达性，并证明事件预测自动机无需模拟即有限。
一点非确定性使下推自动机兼具表达力与简洁性
研究历史确定性下推自动机（HD-PDA）的表达力与简洁性，证明其强于确定型 PDA 但非全部上下文无关语言。
使用加权子图计数的图变换系统终止性
提出通过加权子图计数证明 PBPO+ 图变换系统终止性的方法，支持非线性规则并推广到 SqPO 与左线性 DPO。
基于图变换系统的高阶变换方法用于 BPMN 的形式化与分析
提出基于高阶变换将 BPMN 模型映射为图变换系统，以形式化执行语义并支持行为性质检查。
revTPL：可逆时序进程语言
提出可逆时序进程演算 revTPL，将因果一致可逆性与离散时间/超时机制结合，并证明其满足因果一致可逆性质。
Transpension：Π 类型的右伴随
提出 transpension 类型作为 shape 上全称量化的右伴随，并给出类型规则与 presheaf 语义。
论推理框架的相对渐近表达力
该论文提出推理框架相对渐近表达力的预序，证明两个新的公式渐近等价结果并给出收敛律推论。
顶点完整性的细粒度元定理
建立了以顶点完整性为参数的 FO/MSO 逻辑细粒度元定理及其 ETH 下界。
量子计算的二进片段中 Sum-Over-Paths 的重写与完备性
为 Sum-Over-Paths 提出新重写规则，并证明其在 Toffoli-Hadamard 及二进量子片段上的完备性。
模糊关系与广义度量空间的通用定量代数
将定量代数推广到模糊关系和广义度量空间，不要求运算非扩张，并建立完备证明系统、自由代数与单子性结果。
迈向 QBF 中的统一认证
提出策略提取模拟技术，证明扩展 QBF Frege 可 p-模拟多种子句 QBF 证明系统，支持 QBF 求解统一认证。
具有期望停时的随机过程
研究带期望停时的随机过程优化，证明精确问题与Positivity问题互约，并给出近似求解的复杂度上界。
使用边界模型对分散不确定日志进行离线与在线能效监控
提出基于非线性动力系统过近似边界模型的日志监控方法，支持离线安全违例检测与在线节能采样。
节点复制：理论与实践
提出实现高阶节点复制的项演算，统一刻画按名调用与完全惰性按需调用并证明两者观察等价。
判定 Time Warp 代数中的等式
证明缺少有限模型性质的 Time Warp 代数仍具有可判定等式理论，并给出基于 Z3 的判定实现。
带合取数据库查询的线性规划
提出 LP(CQ) 语言，并用广义超树分解因子化答案集元素，以更少变量高效求解合取查询定义的线性规划。
Galois 连接关联 call-by-value 与 call-by-name
用 call-by-push-value 与 Galois 连接刻画传值与传名的可观察行为关系。
SHACL 特性的表达力及面向完全相等与不相交测试的扩展
证明 SHACL 的相等测试、不相交测试、闭包约束与目标限制各自本原，且完全相等/不相交扩展严格增强表达力。
（无名）哑元的变量绑定与替换
提出 de Bruijn 无名哑元的变量绑定与捕获避免替换新理论，并建立其与 Fiore–Plotkin–Turi 方法的强形式联系。
TT^□_C：一族具有连续性效应实现子的外延类型理论
提出一族外延类型理论，可在系统内用引用单元等有状态计算直接实现连续性原则。
动力系统的鲁棒不可计算性与鲁棒动力系统的可计算性
构造局部稳定却使吸引域鲁棒不可计算的可计算系统，并证明紧集上结构稳定全局稳定平面系统的吸引域可计算。
论带数据的局部一阶逻辑的可满足性
研究带数据局部一阶逻辑片段的可满足性，给出半径1片段可判定及存在片段复杂度全景。
带广义应用的 λ 演算的一种忠实且定量的远距离归约概念
提出 λJn 演算，用远距离归约替代置换转换，以非幂等交类型系统刻画强规范化，并给出到显式替换的忠实翻译。
简单类型可转换性即使对安全 λ-项也是 TOWER-完全的
证明简单类型 λ-项的可转换性问题在 Blum-Ong 安全 λ-项片段上仍是 TOWER-完全。
QBF Merge Resolution 强大但不自然
证明 QBF Merge Resolution 相对 LD-Q-Res、LQU+Res、IRM 有指数优势，但它在限制下不封闭，因而非自然。
公平异步会话子类型
提出公平异步会话子类型，可在无界消费前提前发送，并证明其不可判定、给出可靠算法与实现。
Refl-Spanners：一种处理非正则核心 Spanner 的纯正则方法
将字符串相等选择内嵌进正则语言，提出 Refl-Spanners，以略弱表达力换取更好的静态分析与查询求值上界。
Petri 网的 home-space 问题及其 Ackermann 复杂度
证明 Petri 网半线性 home-space 问题可判定，并给出 Ackermann 完全性。
构造类型论中 Tennenbaum 定理的分析
在构造类型论中重访、推广并机器化验证 Tennenbaum 定理，并揭示经典证明在假设与结论上的差异。
Büchi 博弈的半环溯源：基于吸收多项式的策略分析
用半环语义求值 Büchi 博弈的不动点公式，提取吸收主导策略并支持博弈合成与最小修改分析。
经典项演算的强互模拟
为 Parigot λμ 演算提出修订演算 ΛM 及关系 ≃，证明其关于归约构成强互模拟。
论带假设的 Kleene 代数完备性工具
提出模块化证明 Kleene 代数带假设完备性的工具，并用于 KAT、KAO、NetKAT 及新变体。
论 Skolem、正性与最终正性问题的鲁棒性
研究线性递归序列在初始配置邻域内规避零或负值的鲁棒变体，刻画其可判定性与复杂度边界。
分支良结构迁移系统及其扩展
提出分支良结构迁移系统，放宽良拟序与单调性，保持有界性/非终止性可判定，并界定覆盖性可判定边界。
面向连续随机过程的度量时序逻辑
证明连续时间MTL对随机过程的可测性，并给出离散化概率收敛条件。
流演算的隐函数定理
为流演算中的多项式方程组建立隐函数定理，并展示其相对于经典隐函数定理的计算优势与应用。
从隐式规约合成嵌套关系查询：模型论与证明论视角
证明嵌套关系隐式定义可有效转换为 NRC 显式查询，并给出模型论与证明论构造。
算术 μ-演算的余代数可满足性检查
在更一般的单步逻辑可满足性假设下，给出算术余代数 μ-演算可满足性检查的指数时间上界与通用全局缓存算法。
孤立子序及其在闭包算子计数中的应用
通过孤立子序的商构造建立闭包数量关系，并给出递归计数闭包算子的方法。
带递归模态逻辑的复杂度结果：通过翻译与 tableau
通过翻译与 tableau 统一经典模态逻辑及其递归扩展的复杂度，并给出通用的 2EXP 可满足性上界。
基于时间线的博弈的控制器合成
为基于时间线的博弈提出有效且计算最优的控制器合成方法，填补从获胜策略到可执行控制器的空白。
高阶异步效应
提出高阶异步效应，将操作调用解耦为信号与中断，用核心演算统一异步与代数效应。
锥论中的重心存在性定理
证明局部凸紧 sober 拓扑锥上连续赋值必有唯一连续重心，且恰为扩展赋值单子的 V_w-代数结构。
λ-演算的合理空间代价模型：对数空间
提出基于 Krivine 抽象机变体的 λ-演算合理空间代价模型，首次支持对数空间，并迁移到 call-by-value。
具有社会福利与时序逻辑约束的并发博弈均衡设计
提出均衡设计框架，通过激励使并发博弈的Nash均衡满足LTL/GR(1)时序性质，并给出复杂度界。
统一立方类型论与多模态类型论
将多模态类型论的模态机制与立方类型论的计算良好同一类型结合，建立立方模态类型论并给出模型语义。
操作逻辑关系的纤维化视角：纯、效应与微分
用纤维化统一基于操作语义的逻辑关系，覆盖纯、效应与微分情形。
Scoped Effects 与 Handlers 的演算
提出原生支持代数与 scoped effects/handlers 的演算 λ_sc，含多态处理器、转发子句及类型-效应系统与推断。
可逆 CCS 的真并发语义
通过将 CCS 到 Petri 网的编码与因果一致可逆性结合，为可逆 CCS 给出真并发网语义。
高维自动机的 Kleene 定理
证明高维自动机识别的语言恰为有限区间 pomset 的有理且 subsumption-closed 集合，并建立相应 Kleene 定理。
有限模型论中的卵石关系余单子
引入卵石关系余单子，以其余代数刻画路径宽度，并建立其与 k 变量无穷逻辑受限合取片段的 Lovász 型定理。
ZX 图的加法与微分
提出ZX图加法的归纳定义，并据此给出ZX图的归纳微分，另提供基于变量隔离的非归纳微分及Ising哈密顿量图表示。
在博弈语义中分离并行与干扰
为共享状态并发博弈语义构造因果模型，分离并行与干扰，得到四个完全抽象结果并扩展语义立方体。
组合式合流性判据
将基于递减图的合流性判据推广为可组合形式，并给出消去无关重写规则的约简方法。
线性时间逻辑：一种余代数视角
用余代数统一构造线性时间逻辑，并证明逐步语义与路径语义等价。
Tarski 关系代数的保持定理
研究 Tarski 关系代数若干语义片段的有限生成性，证明同态安全片段可有限生成，而函数保持等片段不可。
异步基于会话的并发：循环进程网络中的无死锁性
提出支持循环网络异步通信的会话类型框架 APCP 与并发 λ 演算 LASTn，并保证无死锁。
多结构博弈及其扩展
精细分析多结构博弈，并引入量词–变量树博弈与语法博弈，同时刻画一阶逻辑的量词数和变量数。
Stabbing Planes 中组合原理的深度下界
提出反链与覆盖两种几何方法，为 Stabbing Planes 证明系统给出组合原理的大小与深度下界。
布尔比例
在通用代数类比比例框架下研究布尔域比例，并证明其与文献中两种著名模型一致。
面向异步不可靠广播通信的会话类型系统
提出不可靠广播会话演算及其会话类型系统，保证同步端点间的健全性、安全性与进展，并支持无确认恢复。
论带有表达性局部 Presburger 约束的二变量守卫片段逻辑
证明带局部 Presburger 量词的二变量守卫片段可满足性是 EXP 完全，并给出简单确定性图算法。
确定性 Büchi 自动机所识别的半位置目标
刻画了确定性 Büchi 自动机识别且为半位置的目标，并给出多项式时间判定算法。
直谓 Bishop-Cheng 测度论中的预测度空间与预积分空间
在 Bishop 集合论中引入直谓的预测度空间与预积分空间，为 Bishop-Cheng 测度论提供可预测性重构。
十年后再论安全博弈
给出图上安全目标策略所需最小记忆状态数的精确刻画：等于左商语言包含极大反链的大小。
一元确定的分配 ℓ-magma 簇与束蕴涵代数
刻画一元确定分配 ℓ-magma 的簇结构，并将其应用于束蕴涵代数的模型与有限模型构造。
稳定化 profunctor 与结构的稳定 species
通过给 groupoid 加 kit 来稳定 profunctor，建立线性逻辑的双范畴模型，并证明稳定 species 双范畴笛卡尔闭。
时序邻域算子的加入使前缀与子区间逻辑变为 EXPSPACE-完全
证明在 BD_hom 中加入对应 Allen 关系 Meets 的时序邻域模态 A 后，所得 BDA_hom 的可满足性为 EXPSPACE-完全。
带计数的不动点逻辑中 Unique Games 的不可近似性
证明 FPC 无法以任何常数因子近似 Unique Games 的最优值，并给出新的不可近似间隙。
探索具有描述逻辑特征的命题动态逻辑的非正则扩展
证明 ALCvpl 加入 Self、nominal 或非正则查询原子后，可满足性与查询蕴涵不可判定。
信息流逻辑中的可执行一阶查询
提出 FLIF，将 LIF 的一阶片段用于受限访问模式查询，等价于可执行一阶逻辑并翻译为查询计划。
通过抽象机将 λ-演算完全抽象地编码到 HOcore 中
通过抽象机将按名/按值 λ-演算及 λμ-演算完全抽象地编码到最小高阶进程演算 HOcore。
semi-primal 簇上的多值余代数逻辑
提出将经典余代数逻辑沿 semi-primal 真值代数簇提升为多值逻辑的系统方法，并保持一步完备性与表达性。
游戏余单子与广义量词
将游戏余单子推广到含广义量词的逻辑，用双参数余单子刻画 Hella n-双射 k-石子游戏，并给出范畴语义与新型树分解。
使用高阶捷径规则的高级模型一致性恢复
提出在模型同步过程中即时计算高阶捷径规则，避免信息丢失，并在 eMoflon 中实现与评估。
严格化与相干性的弦图
为非严格幺半范畴给出弦图生成元与关系表示，并由此给出 Mac Lane 严格性与相干性定理的图形化证明。
论 iso- 与 equi- 递归类型的语义表达力
证明带 iso- 与 equi- 递归类型的 STLC 语义表达力相同，且都等价于项级递归 STLC。
通过结构化 λ 演算的策略空间证明 eval-readback 与 eval-apply 大步求值器的等价性
在良构、统一策略与平衡混合策略条件下，证明 eval-readback 与 eval-apply 大步求值器一步等价，并厘清 λ 演算策略空间。
Twin-width 与排列
证明二元关系结构类具有有界 Twin-width 当且仅当它是某个真排列类的一阶转换。
量子系统的可编码性准则
检验经典编码质量准则在量子进程演算中的适用性，给出 CQP 风格语言到 qCCS 风格语言的编码并证明其性质与反向不可编码性。
确定性下推自动机可压缩某些正规序列
构造确定性下推转换器，并证明它能压缩某个正规数字序列，从而正面回答一个开放问题。
202395 篇 · vol.Volume 19, Issue 2
推断符号自动机
研究符号有限状态自动机（SFA）的可学习性，给出查询学习与极限可识别性的正反条件及规模度量。
一个在不可预测环境中度量程序鲁棒性的框架
提出基于随机变量序列与概率分布度量的程序鲁棒性框架，并定义适应性与可靠性及统计推断评估算法。
验证基于效应处理器的 define-by-run 反向模式自动微分库
对基于效应处理器的 define-by-run 反向模式自动微分库，给出机器检查的正确性证明。
智能选择与选择单子
用选择单子为含选择、奖励与概率的语言建立操作/指称语义，并证明二者一致与完全抽象。
融入语义性质的结合交换同余闭包算法的模块化与组合
提出模块化 AC 同余闭包算法，可组合幂等、可消去、群等语义性质，便于集成到 SMT 求解器。
递归概率程序时序性质的模型检测
给出概率下推自动机对 ω-可见下推语言（如 CaRet 可描述的性质）模型检测的可判定性与复杂度结果。
阈值自动机与 Byzantine Model Checker 的参数化验证综述
综述用阈值自动机和 ByMC 对阈值守卫容错分布式算法进行参数化自动验证的技术。
基于划分精化的双模拟判定算法下界
证明了使用划分精化的顺序与并行双模拟判定算法的时间下界，分别为 Ω((m+n) log n) 与 Ω(n)。
向 λμ-演算中添加否定
在 Parigot 的 λμ-演算中引入否定类型构造及语法构造，并证明其归约合流、强规范化与主类型性质。
不动点理论——颠倒视角
提出证明元素高于最大不动点或低于最小不动点的证明规则，并用有限逼近与 MV-代数格统一处理概率/度量语义及随机博弈。
SAT 启发的高阶消去技术
将多种命题预处理消去技术推广到高阶逻辑，提出拟纯文字消去，并在 Zipperposition 中提升自动证明搜索。
灵活的正确性构造编程
提出并形式化两种更灵活的构造正确编程方法 CbC-Block 和 TraitCbC，并比较其可用性。
证明无关命题类型的无归约规范化
为含宇宙层级与证明无关命题的类型理论给出无归约规范化及转换可判定性证明，且无需显式中性与范式。
从停机问题到半合一的构造性多一归约（扩展版）
给出停机问题到半合一的构造性多一归约，并用无公理 Coq 机械化证明其 RE 完全性。
通信有限状态机的可同步性是不可判定的
证明 peer-to-peer 通信有限状态机的可同步性不可判定，并给出有向环拓扑下可判定
HyperATL*：多智能体系统中超属性的逻辑
提出带策略量词的 HyperATL* 超逻辑，统一表达多智能体系统的策略性安全属性，并建立可判定且渐近最优的模型检测方法。
Good-for-games ω-下推自动机
引入 good-for-games ω-下推自动机，证明其比确定性 ω-PDA 表达力更强，且相应无限博弈求解为 EXPTIME 完全。
一阶分支时间属性的双向运行时强制
提出双向运行时强制的操作框架，并证明带递归的Hennessy-Milner逻辑安全片段sHML可由动作禁用监视器强制。
正则 Trail 查询的三分法
证明固定正则表达式下 trail 语义 RPQ 求值的复杂度三分法，并刻画可处理类 Ttract。
Arboreal 范畴：资源的公理化理论
提出公理化的 Arboreal 范畴与覆盖，统一有限模型论中的双模拟、来回博弈及资源计数。
面向单纯形模型的空间逻辑
提出在单纯复形上解释的空间逻辑，给出线性复杂度的模型检测算法，并用双模拟刻画其表达力。
交互与结构系统 III：BV 与 pomset 逻辑的复杂度
证明 pomset 逻辑与 BV 并不相同，并确定二者可证性复杂度分别达 Σ₂^p-完全与 NP-完全。
结构无歧义概率文法的学习
提出查询学习算法，可同时学习结构无歧义概率上下文无关文法的文法拓扑与概率权重。
有限状态自动机的弦图有限公理化
用弦图语法为有限状态自动机建立有限完全等式理论，并证明 Kleene 星可派生。
论单值基础中的小类型
在构造性单值基础中证明非平凡完备偏序集必然是大类型，并揭示 Tarski 定理的谓词式限制。
形式编排语言理论
提出形式编排语言元模型，统一刻画消息传递系统的全局/局部视图、投影正确性与通信性质。
正则表达式抽取结果上聚合操作的复杂度
系统分析正则文档跨度器上聚合查询的精确与近似计算复杂度，并给出多项式时间与 FPRAS 边界。
字母到字母转换器的轮次模拟
提出转换器的轮次模拟与轮次等价，并判定给定 k 及存在 k 时的模拟问题。
优先化最佳变体
提出 Priority GV，将通道创建与线程生成解耦，用优先级类型系统恢复环状进程的死锁自由，并给出 PCP 编码。
相干微分 PCF
提出确定性微分 lambda 演算，基于非加性范畴语义，将 PCF 扩展为完全确定性的微分语言。
FTMPST：容错多方会话类型
将容错机制引入多方会话类型，支持不可靠通信与进程崩溃，并用失败模式增强进程语义以分析分布式算法。
指数作为替换与线性逻辑中切消去的代价
提出指数替换演算 ESC，为 IMELL 切消去给出具子项性质的多项式代价模型，并证明合流与强规范化。
范畴论可组合密码学：扩展版
用范畴论形式化密码学模拟范式，证明抗抽象攻击的协议构成对称幺半范畴，并给出可组合安全性的抽象模型。
安全与余安全语言的一阶逻辑刻画
提出 FO-TLO 的 SafetyFO/coSafetyFO 片段，精确刻画 SafetyLTL 与 coSafetyLTL 并给出表达力结果。
Guarded TGDs 下的答案计数
为 guarded TGDs 本体/约束下的答案计数给出参数化复杂度分类，并研究结构测度有界性元问题。
运算符优先级语言的非周期性、星自由性与一阶逻辑可定义性
将正则语言中星自由、非周期与一阶逻辑可定义性的经典等价推广到运算符优先级语言。
用于半环上加权自动机双模拟的余代数
在半模范畴与集合范畴中用余代数终余代数刻画半环加权自动机的加权语言等价与加权双模拟。
一种强 call-by-need λ-演算
提出支持强归约的 call-by-need λ-演算，保证按需且至多一次求值，并证明强规范化与最小归约策略。
LNL polycategory 与线性逻辑的 doctrine
引入 LNL polycategory 与 LNL doctrine，统一刻画含指数的经典线性逻辑及其多种范畴结构。
幺半宽度
提出幺半宽度，作为幺半范畴中态射的复杂度度量，通过幺半分解惩罚大对象复合，统一刻画树宽、秩宽与矩阵秩。
广义度量空间上富集的自治范畴的语法侧
为线性λ演算引入取值于quantale的V-等式演绎系统，证明其可靠完备，并建立其理论与广义度量空间富集自治范畴的等价。
带函数约束的事务模板对 Read Committed 的鲁棒性
为事务模板引入函数约束以提升建模能力，并刻画其对 Read Committed 鲁棒性判定的不可判定性与可处理片段。
图（非）同构验证的证明系统
为 McKay–Piperno 图规范标号算法构建形式证明系统，导出可独立检查的证明以验证图非异构。
故障检测器的参数化验证：一个案例研究
利用对称点对点算法的 cutoff，在 TLA+、IVy 与计数器自动机上参数化验证 Chandra-Toueg 故障检测器的安全性与活性。
可数MDP中逐点收益、平均收益与总收益目标的策略复杂度
完整刻画可数MDP中三类收益目标下ε最优与最优策略所需和充分的内存，给出策略复杂度分类。
时间系统的最优控制器合成
将加权时间博弈的可分析片段扩展到含负权重，证明值仍可近似，并给出可判定子类与值迭代符号算法。
面向 PCTL 的可靠近似与渐近概率互模拟
提出参数化近似概率互模拟，证明其对 PCTL 松弛语义可靠，并扩展为状态族的渐近等价。
寻找无领导者会合协议中的 cut-off 是容易的
证明无领导者会合协议的 cut-off 问题是 P 完全的，对称协议在 NC 中，并改进有领导者对称协议的复杂度上界。
Token 博弈与历史确定性的定量自动机
将 token 博弈扩展到定量自动机，刻画历史确定性并给出多类 HDness 判定复杂度。
倒计时游戏与（简洁）单计数器网上的模拟
证明 succinct 单计数器网上模拟前序为 EXPSPACE 完全，并给出倒计时游戏变体的自包含证明。
枚举独立线性推理
借助线性公式的图形表示高效搜索独立线性推理，发现8变量最小实例并反驳已有猜想。
用无穷对象计算：格雷码案例
在直觉主义不动点逻辑中引入并发版本，证明无穷Gray码表示与带符号数字表示的并发概念等价，并推广到实数非空紧子集超空间。
标准 Borel 空间上相对熵的范畴论刻画
为标准 Borel 空间上的概率分布建立范畴论框架，将相对熵刻画为到 Lawvere 范畴的函子并证其凸性、下半连续与唯一性。
Actor 与灰色故障的模型
提出带灰色故障的 actor 系统模型与弱 barbed 互模拟等价，将可靠性验证归约为互模拟检查。
异步会话的去禁闭全局类型
提出可类型化所有异步多参与者会话的全局类型系统，并给出可靠完备的类型推断算法。
面向邻居的计算：用函数式编程与 Scala 应对大规模分布性与自适应性
提出 neighbours calculus 与“对邻居计算”概念，简化邻域交互的声明式表达，并以 Scala 实现 ScaFi。
理解 QBF CDCL 求解器与 QBF 归结的相对强度
将 QCDCL 形式化为证明系统，证明其与 Q-归结不可比，并给出下界及可指数加速的新决策策略。
桥接因果可逆性与时间可逆性：一种随机进程代数方法
在随机进程演算中给出因果可逆性与时间可逆性同时成立的条件，并引入双向随机互模拟。
类型论的模块化构造
在 λΠ-模理论中构造统一理论 U，使多个逻辑系统的证明可模块化嵌入并保持子理论性质。
社交网络中确认偏差下极化的形式化模型
提出带确认偏差的多智能体信念更新形式模型，刻画社会网络极化最终消失或持续的条件。
平滑地分离会话
提出 Hypersequent GV，用超环境保证会话类型结构同余的类型保持，并与 HCP 建立保持及反映归约的操作对应。
随机博弈中的竞技场无关有限记忆确定性
研究随机博弈中竞技场无关有限记忆策略的充分性，证明其可归约到单玩家随机博弈并给出两组刻画。
非纯单纯复形：完全公理化
为描述非纯单纯复形的三值多主体认知逻辑给出公理化，并证明其可靠性与完全性。
正则路径查询的细粒度复杂度
系统刻画正则路径查询求值中乘积图方法可达到的复杂度上界，并给出细粒度条件下界。
重叠代数作为几乎离散的 locale
提出重叠代数可构造地刻画几乎离散 locale，并在 LEM 下与 Boolean locale 一致。
互模拟语义下的下推自动机与上下文无关文法
在互模拟语义下重新刻画下推自动机与上下文无关文法的对应，指出需引入状态感知才能恢复完整对应。
通过自组织的空间流体自适应采样
提出基于场协调的自组织自适应采样算法，通过动态竞争区域划分空间，并证明其自稳定与局部最优。
多方测试预序
提出无协调与个人主义两种多方测试预序，刻画其相对经典 must 测试预序的粗细关系及装饰迹表征。
Lacon-、Shrub- 和 Parity-分解：刻画有界扩张类的转导
用 lacon、shrub 与 parity 分解刻画有界扩张类的转导，并将结构有界扩张类编码到有界扩张类。
带交与常元的关系模型：Lambek 演算的关系语义
研究带交与零/单位常元的 Lambek 演算关系语义，厘清其弱/强完全性的成立边界。
无环查询的重写：注意头部（Mind Your Head）
证明若合取查询 Q 存在重写，则当 Q 无环时也存在无环重写，并厘清无环视图重写问题的可处理边界。
子词序上的存在可定义性
证明字母表大小至少 3 时，子词序结构存在片段可定义的关系恰为递归可枚举关系，并刻画所有量词交替层级。
并发过程历史与资源转换器
用 proarrow equipment 的字符串图刻画并发过程产生的物质历史，并构造资源转换器范畴。
因果展开与析取原因
通过扩展素事件结构并引入等价关系，构造一般事件结构的因果展开，证明其为伪右伴随。
带非一元计数量词的 Presburger 算术
证明带元组模/阈值/精确计数量词的 Presburger 算术可判定，并给出双指数空间与交替时间上界。
词与图上的正一阶逻辑
证明正一阶逻辑 FO+ 在有限词与图上表达力受限：Lyndon 保持定理失效，且正则语言的 FO+ 可定义性不可判定。
平均支付博弈中的子博弈完美均衡（期刊版）
引入需求与协商函数，刻画平均支付博弈的所有子博弈完美均衡，并证明SPE阈值问题可判定。
小字母表上概率自动机的判定问题
按歧义度与字母表大小刻画一元/二元概率自动机空性和λ-可达性的复杂度。
有限有界 Petri 网中两种真并发等价关系的可判定性
证明完全并发互模拟与 i-因果网互模拟在有限有界 Petri 网上可判定，推广了安全网结果。
任意关系演算查询的高效求值
提出将任意关系演算查询翻译为两个安全范围查询，再转成SQL，从而借助标准DBMS高效求值并改进复杂度。
流处理器与余模型
用代数效应的余模型统一刻画外延与内涵流处理器，并类比双模拟与迹等价。
名义 PROPs 的完备性
将字符串图内化到名义集合范畴，定义名义 PROPs，并证明其与普通 PROPs 范畴等价以迁移完备性。
非标准分析的有状态 realizer
为半直觉主义非标准算术提出带状态 λ-演算的可实现性解释，并给出 Idealization 与 LLPO 的非平凡 realizer。
Milner 正则表达式模互模拟证明系统的余归纳重构
提出 cMil 余归纳重构，替代 Mil 的不动点规则，并证明两者定理等价。
二阶修正 Krom 逻辑刻画多项式层级
证明二阶修正 Krom 逻辑及其片段可逐层刻画多项式层级，并给出捕获 NL 与 co-NP 的新逻辑。
连续位置收益
证明连续收益的位置确定性与前缀单调性等价，并用三种技术给出证明及算法结果。
非确定性函数作为非确定性进程（扩展版）
提出 lambdafail 到 spi 的带类型编码，用会话类型刻画非确定与失败求值的对应。
局部性与中心性：簇 ZG
证明群元素均中心的幺半群簇 ZG 是局部的，并将其语言刻画为单例语言与正则交换语言的不交混洗的有限并。
树代数的幂集构造
证明线性树单子与上闭幂集单子之间存在分配律，并证非线性情形不存在。
使一阶线性逻辑成为生成文法
证明范畴语法所在的 MLL1 片段等价于扩展张量类型演算 ETTC，并给出无切矢列演算与自然演绎。
计算线性递推序列正性集的密度
证明可以任意精度计算线性递推序列正性集的密度，并可判定其是否为零或一，且推广到线性动力系统的符号轨道。
交换半环上加权交替自动机的 Nivat 定理
在交换半环上给出加权交替自动机的 Nivat 型刻画，并联系多项式自动机与 ZERONESS 可判定性。
动态 Cantor 导数逻辑
为动态拓扑系统中的 Cantor 导数模态逻辑建立有限模型性质与完备性证明方法。
通过 Taylor 展开对无穷 β-归约的有限模拟及其应用
为无穷 λ-演算 Λ∞^{001} 建立 Taylor 展开，用资源演算的有限归约模拟无穷 β-归约并证明广义交换定理。
层次查询的静态与动态求值中的权衡
通过按值度数采用轻重策略，统一刻画层次查询在静态与动态求值中预处理、更新与枚举延迟的权衡。
2022118 篇 · vol.Volume 18, Issue 2
用于 SAT 求解器-精化器通信的灵活证明格式
提出 FRAT 证明格式与工具链，显著降低 UNSAT SAT 证明精化为 LRAT 的时间与内存开销。
一种拟多项式时间求解奇偶博弈的递归方法
提出 Zielonka 递归算法的改进，将奇偶博弈求解复杂度降至拟多项式时间。
高阶函数的高阶自动微分
为高阶语言中的前向模式自动微分建立基于 diffeological spaces 的语义正确性证明，并扩展到高阶导数。
依赖类型理论的可扩展相等性检查算法
提出一种用户可扩展的相等性检查算法，适用于一大类依赖类型理论，并在 Andromeda 2 中实现。
概率重写与渐近行为：终止性与唯一范式
为概率重写系统建立分析终止性、唯一极限分布与唯一范式的证明技术，并用于比较归约策略。
在 Event-B 的 institution 中构建规约
为 Event-B 规约语言建立基于 institution 的形式语义，证明其满足性保持与模型合并条件，并统一参数化与精化等模块化构造。
协变与逆变：对一个老问题的新审视（供函数式程序员学习的进阶类型系统入门）
重新审视面向对象方法参数的协变/逆变特化，论证二者可在同一语言中共存，并以实例讲解进阶类型系统概念与实现技巧。
基于模型检测的计时自动机鲁棒性分析
针对时间常数不确定与受扰动的计时自动机，提出若干概念与技术，用模型检测分析其鲁棒性并辅助设计阶段的常数额定。
反例引导的预言（prophecy）用于模数组理论的模型检测
通过自动添加预言变量并结合反例引导抽象精化，将含数组与量词不变式的模型检测归约为无量词、无数组的归纳推理。
EUF 中的一致插值：使用 DAG 表示的算法
提出两种基于项 DAG 表示的算法，用于在 EUF 中计算无量词一致插值，并给出正确性与完备性证明。
Riesz 空间与模态 Riesz 空间的证明论
为 Riesz 空间与模态 Riesz 空间设计超序列演算，证明可靠、完备与切消，并据此给出模态 Riesz 空间可判定性的新证明。
Coq 中的希尔伯特第十问题（扩展版）
在 Coq 中完成 DPRM 定理的首次完整机器化证明，形式化了希尔伯特第十问题的不可判定性。
定量验证中的比较器自动机
提出比较器自动机，统一比较两条无限权重序列的聚合值，并用于定量验证算法。
通过因子分解系统与实例的极小性概念
在带因子分解系统的范畴中统一刻画余代系统的极小性与最小化，并给出可达性与可观测性最小化及可顺序化条件。
DeFi 中自动做市商的理论
提出 AMM 的抽象操作模型，形式化证明其结构与经济性质，并给出套利问题的一般解。
一种用于监控空间分布式信息物理系统动态网络的逻辑
提出并扩展STREL时空逻辑，为动态空间分布式CPS提供定性与定量语义及离线监控算法。
连续空间的几何模型检测
提出连续空间上空间逻辑 SLCS 的几何语义与基于多面体的模型检测工具 PolyLogicA。
可在 arena-independent 有限内存下最优博弈的游戏
完整刻画了允许双方用与竞技场无关的有限内存取得最优策略的偏好关系。
Actris 2.0：分离逻辑中基于异步会话类型的推理
提出 Actris 2.0，将异步会话类型协议与并发分离逻辑结合，支持子协议，并用 Coq/Iris 验证消息传递并发程序。
商类型、归纳类型与商归纳类型
在构造类型论中引入 QWI 类型，并证明其可由商类型与归纳类型导出，Agda 机器化验证。
GFG transition-based 自动机的最小化与规范化
提出 GFG co-Büchi 迁移接受式字自动机的多项式最小化算法，并证明最小自动机可规范化。
Rast：一种资源感知会话类型语言
提出并实现 Rast 语言，用算术细化、ergometric 与 temporal 会话类型刻画并发程序的工作量和跨度，并自动重构类型信息。
时空作弊检测中的符合关系与超属性
提出面向信息物理系统的广义无作弊性概念及 HyperSTL* 超属性时序逻辑，用于时空域符合性监测与作弊检测。
一种面向 Bishop 集合的立方语言
提出 XTT——面向 Bishop 集合的笛卡尔立方类型论，使所有类型满足定义性 UIP，并证明 canonicity。
酉球中的量子控制：Lambda-S1 及其范畴模型
为量子λ演算 Lambda-S1 选取有效类型规则，并用值分布范畴与集合范畴的伴随给出范畴语义。
通过模糊松弛扩展刻画行为半度量的特征逻辑
在通用余代数框架下用模糊松弛扩展统一构造行为距离的特征模态逻辑，并覆盖非对称半度量。
非确定性、概率与终止系统的迹理论
通过余代数广义幂集构造统一刻画非确定性、概率与终止系统的迹等价，并与既有定义比较。
面向结构化上下文无关语言的一阶完备时序逻辑
提出基于算子优先语言（OPL）的时序逻辑 POTL，证明其一阶完备性，表达力优于 NWTL 与 OPTL。
完整性约束再探：从精确蕴含到近似蕴含
定义满足度上的近似蕴含，研究数据库依赖与概率条件独立的精确蕴含何时能松弛为线性不等式。
验证递归比特币合约的流动性
提出 BitML 合约流动性的有限状态抽象与模型检测方法，并实现自动验证与编译工具链。
模块化验证持久不透明性
将持久不透明性验证模块化，分离持久性证明与不透明性证明，并给出 NOrec 的持久不透明版本。
分配律的不可能性定理
提出三类判定两个 monad 间不存在分配律的定理，统一既有 no-go 结果并解决 list monad 自分配等开放问题。
同质性假设下子区间逻辑的可满足性与模型检测
证明同质性假设下子区间逻辑 D 的有限可满足性与模型检测均为 PSPACE 完全，拓展了易处理区间时序逻辑。
实例可归约性与 Weihrauch 度
提出实例可归约性，证明实例度构成 frame，并推广为结构更丰富的扩展 Weihrauch 度。
高阶语言中应用型互模拟同余性的范畴论框架
提出范畴框架，抽象证明应用型互模拟自动同余，统一Howe格式下高阶语言。
无限概率数据库
提出用有限点过程为无限概率数据库建模，并证明关系代数、聚合与 Datalog 查询在不可数概率空间中的可测性。
可扩展的去中心化 Actor 终止检测算法
提出 DRL：基于异步本地快照与消息传递的去中心化 actor 终止检测算法，支持垃圾回收并容忍网络分区。
Big-O 问题
研究加权自动机间的 Big-O 关系，证明其一般不可判定，并给出多个可判定子类的复杂度。
超越记号：定理证明语言的卫生宏展开
提出面向交互式定理证明器的卫生宏系统，同时解决意外名称捕获与语法扩展能力不足，并集成到 Lean 4。
一次性判定所有行为等价：线性时间—分支时间谱系中的博弈
提出统一博弈，可在 van Glabbeek 线性时间—分支时间谱系中一次性判定两进程的行为等价关系。
图上的分析性命题证明系统
提出一种在图而非公式上操作的分析性命题证明系统，利用图模块分解与深推理证明切可容许性，并保守扩展带 mix 的乘法线性逻辑。
带 Church 论题与选择公理的归纳与余归纳拓扑生成
证明在最小主义基础中加入余归纳定义以生成正拓扑，不提高相对 CZF+REA 的一致性强度。
一个刻画可行泛函的分层类型编程语言
用分层类型系统为带 oracle 调用的命令式语言刻画 BFF2，类型推断可判定且复杂度为三次方。
基于 BDD 的边着色图强连通分量（SCC）分解算法
为边着色图提出基于 BDD 的符号 SCC 分解算法，最坏 O(p·n·log n) 符号步。
可互操作医疗系统中时间性质的规约与验证
用 Timed Rebeca 形式化建模医疗设备通信模式并模型检测时间性质，提出基于模式静态性质的可靠状态约简。
无限字上可计算正则函数的合成
对无限字正则函数证明可计算当且仅当连续，并给出判定与合成图灵机的过程。
Monad 上的模与操作语义（扩展版）
推广 reduction monad 提出 transition monad，为操作语义提供高层代数规范工具，覆盖多种演算与 GSOS 格式。
异步共享内存程序的一般可判定性结果：高阶及更高阶
从语言理论视角给出异步程序安全、终止与有界性验证的通用可判定/不可判定边界，覆盖高阶情形。
信息抽取中的权重标注
将文档 spanner 扩展为 annotator，用 provenance 半环为抽取结果标注权重，并研究加权 VSet 自动机的表达力与枚举复杂度。
顺序关系分解
形式化按输入/输出关系描述的规范顺序分解问题，并刻画其在不同表示下的计算复杂度。
并发行为的异步圈积与级联分解
提出异步圈积与异步级联分解，将Krohn-Rhodes理论推广到Mazurkiewicz迹与异步自动机。
一致包络
提出一致包络，为不连续函数上连续可得信息提供一致可计算的因子分解与复合定理。
析取基：模态逻辑的范式与模型论
系统研究余代数模态逻辑中的析取基概念，建立模拟定理、Lyndon 定理与一致插值等范式与模型论结果。
带 Corules 的推理系统：二元会话类型的安全性-活性组合性质
提出带 corules 的广义推理系统，统一刻画二元会话类型的组合安全性与活性性质，并给出可靠完备且更简单的刻画。
行为不等价的通用模态见证的拟线性时间计算
提出在余代数框架下通用构造区分行为不等价状态的模态公式的拟线性时间算法，统一覆盖多种迁移系统。
面向 [D]^k→Z^d 中无序数据向量的线性方程
将线性方程推广到从无序数据集合的 k 元子集到整数向量的数据向量，并证明非负整数解在 NEXP、整数解在 P。
非确定性名义自动机的剩余性与学习
提出 residual nominal automata 子类，证明其规范表示可由有限观察构造，从而支持主动学习。
参数化时间自动机中的可达性与活性
为参数化时间自动机及其子类的可达性与活性问题划定了新的可判定性边界并给出复杂度结果。
二阶计算规则的模块化终止性证明及其在代数效应处理器中的应用
提出二阶计算规则的模块化终止证明方法并实现工具SOL，用于代数效应处理器的CBPV演算终止性。
可熔数（Fusible numbers）与皮亚诺算术
定义可熔数，证明其序型为 ε₀，并给出 PA 无法证明的真命题与终止性实例。
寻址机作为 λ-演算的模型
提出寻址机及其基于最左归约的操作语义，并将地址集构造成组合代数，从而为完整无类型 λ-演算提供模型。
概率相干空间中的微分与距离
在概率相干空间中用导数刻画 pPCF 执行时间期望，并证明态射 Lipschitz 性以连接观测距离与模型距离。
类型化调用上下文的函数式抽象
通过 CPS 语义中调用迹的函数式表示，为 control/prompt 推导出恰好编码 CPS 约束的类型系统。
由同调方法获得的重写规则数量下界
用同调方法改进项重写系统的重写规则数下界，并实现计算与实验。
反应式系统的条件互模拟
在 Leifer-Milner 反应式系统中引入条件互模拟，给出等价定义并比较相关行为等价。
有限结构极限的对偶理论视角（扩展版）
通过 Stone–Priestley 对偶与模型论类型，为有限结构极限建立带概率算子的扩展逻辑及可靠完备演算。
论并行组合的可公理化性
在 BCCSP 中为交错并行组合的多种模拟与踪迹语义给出有限完备公理化，并证明嵌套踪迹/模拟语义不可有限公理化。
有界自然函子的商
提出商类型继承 BNF 结构的充分条件与更一般提升方案，并在 Isabelle/HOL 中自动化商类型的 BNF 注册。
非传递关系的不动点定理
在 Isabelle/HOL 中形式化序论不动点定理，将完备序结果推广到仅需反对称性或吸引性的非传递关系。
经验证的近似算法
首次对多个 NP 完全优化问题的近似算法进行形式化验证，发现已有证明的不完备性并改进了一个近似比。
多面体面格的形式化
在 Coq 中首次形式化多面体的面，证明面构成分级原子/余原子格并验证 Balinski 定理。
Coq 中的 Trakhtenbrot 定理：构造视角下的有限模型论
在 Coq 中机械化有限一阶可满足性的可判定性分类，证明 Trakhtenbrot 定理并归约到分离逻辑。
二进制带符号数字表示中实数的极限
从构造性证明中提取经形式验证的精确实数极限计算算法，并在 Minlog 与 Haskell 中实现。
通过弱分配律的凸性
该文将幂集到半模单子的弱分配律刻画为自由半模中的凸闭包，并复合得到凸子集单子。
余代数几何逻辑：基础理论
用余代数统一框架为命题几何逻辑添加模态，并建立其推导系统、完备性与行为等价理论。
循环证明作为会话类型化进程：一个局部有效性条件
将带最小/最大不动点的子结构逻辑循环证明解释为会话类型进程，并给出可判定的局部有效性条件。
对布尔公告的量化
提出 BAPAL，将 APAL 的公告量化限制为布尔公式，给出有穷公理化并证明其表达力弱于 APAL。
函数依赖不一致性度量的 Shapley 值
系统研究函数依赖违反下常见不一致性度量的 Shapley 值计算复杂度，给出可处理与难处理类的完整分类及近似复杂度结果。
面向量子编程语言的线性依赖类型论
提出基于幺半范畴纤维化的线性依赖类型论，并将其集成到量子电路语言 Proto-Quipper-M。
平面弦图的正规化与二次等价算法
证明平面连通弦图的左/右交换均强正规化，给出线性/二次等价判定算法并强化 Joyal-Street 相干性定理。
何时可以使用结果有界的数据接口来回答查询？
将使用结果有界访问方法回答查询的可回答性问题归约为带约束的查询包含问题，并给出常见约束类下的可判定性与复杂度结果。
FIFO 机器中的有界可达性问题是可判定的
提出输入有界欠近似，将 FIFO 机器的有界可达性归约到受限零测试计数器机，证明其可判定。
概率图上同态封闭查询求值的二分性
证明概率图上同态封闭查询求值存在多项式时间与#P-hard之间的完整数据复杂度二分。
无限时长博弈的通用图理论
提出通用图理论，统一构造无限时长博弈的值迭代算法，并改进奇偶与平均收益博弈的时空复杂度。
具有因果记忆的分布式异步博弈是不可判定的
证明异步自动机与因果记忆控制器的分布式控制问题不可判定。
在 MSO 中优化树分解
证明宽度 k 树分解到最优宽度树分解可由 MSO 转换实现，并由此导出线性 FPT 算法。
命题证明复杂度的有限模型论视角
用不动点逻辑精确刻画Horn消解、有界宽度消解与有界次数多项式演算的证明能力。
强规范化的高阶关系查询
为高阶关系查询到 SQL 的翻译所依赖的重写系统补上强规范化证明，并把证明扩展到集合/多重集合异质查询。
无自连接合取查询的均匀可靠性
证明无自连接合取查询的均匀可靠性可多项式求解当且仅当查询是层次的，并推广可靠性二分法。
代数相干合流与高阶球状 Kleene 代数
引入高阶球状 Kleene 代数，将合流证明推广为相干合流，并用等式推理证明相干 Church-Rosser 定理与 Newman 引理。
无限树的正则匹配问题
将 Conway 的正则匹配可判定性结果推广到有限与无限正则树语言，并证明 inside-out 替换下极大解有限且可计算。
幂集余代数的对偶性
证明 CABA 上某自函子的代数范畴与 Set 上幂集余代数范畴对偶，并由 Tarski 对偶推出 Thomason 对偶。
连接二元关系的近优并行算法
提出 MPC 模型下连接二元关系的常数轮近优并行算法，负载达到已知下界（至多 polylog 因子）。
可归约到大 CSP 的小型 Promise CSP
构造可归约到大有限 CSP 的小型 Promise CSP，并给出图情形的正面结果。
函数式与命令式会话类型的关联
通过双向翻译刻画函数式与命令式会话类型演算的表达力差异。
同伦类型论中的 Nielsen-Schreier 定理
在 HoTT 中表述 Nielsen-Schreier 定理，构造性证明有限指数情形，并揭示全定理对选择公理的依赖及反例。
粘合资源证明结构：居留与逆向 Taylor 展开
用重写系统刻画资源证明结构集何时来自 MELL 证明结构的 Taylor 展开，并证明无割 MELL 居留问题半可判定。
寄存器自动机与时间自动机的可确定性
完整刻画寄存器自动机与时间自动机确定性成员问题的可判定性与复杂度版图。
不同数据域上数据词转导的可计算性
研究寄存器转导器定义的数据ω-词函数，证明连续性与可计算性等价，并给出判定问题的PSpace复杂度
关于 λ-项的 Taylor 展开及其刚性逼近项的群胚结构
改进 λ-项 Taylor 展开正规形与 Böhm 树同构的证明，引入刚性资源演算中的置换群胚并扩展到非确定性情形。
立方类型理论的典范性与同伦典范性
在预层模型中以 sconing 论证证明立方类型理论的同伦典范性与典范性。
带极值约束的寄存器自动机及其在二变量逻辑中的应用
引入带极值约束的无限树寄存器自动机，证明其空问题可判定，并用于二变量逻辑可满足性。
低度数据库上一阶查询的答案枚举
论文将低度数据库上一阶布尔查询的伪线性时间判定推广到查询求值，实现答案计数、常时判定与常延迟枚举。
时间 CSP 的可处理组合
证明两个时间结构理论的 CSP 并集要么多项式时间可解，要么 NP 完全。
模态交-蕴涵逻辑
为直觉主义交-蕴涵片段引入保交与单调模态，建立半格语义、对偶、完备性及可表达性结果。
带负权重的单时钟价格时间博弈
证明单时钟简单价格时间博弈可在伪多项式时间内计算最优值与最优策略，并推广至负重置无环情形。
逆外延性与分离性
利用分离关系为逆外延性提供计算解释，并构造装配范畴模型。
形式拓扑中的 σ-locale
证明 σ-frame/σ-locale 可归入形式拓扑，并构造性地刻画最小强稠密 σ-子locale。
命题量化为何使树上的模态与时序逻辑稳健地困难？
证明仅含 EX 的树语义命题量化 CTL 已 Tower 难，并给出有界树上的 AExpPol 完全性及多类模态逻辑的 Tower 难下界。
有序余代数的 Moss 逻辑
为局部单调内函子上的 T-余代数提出有限化 Moss 覆盖模态逻辑，建立基概念并证明 Hennessy-Milner 性质与序列演算完备性。
第三技巧
将石原第一、第二技巧推广到函数序列，证明了一个类似的数学结果。
原子多态中的可类型性与类型推断
证明 Curry 风格原子多态系统 Fat 的可类型性可判定，并给出能处理非冗余约束的类型推断算法。
关于具有给定交集类型的项集
证明每个强规范化 λ 项都有唯一交集类型，并揭示给定类型闭项集的可分离性与数字系统性质。
CC-电路与幂零代数的表达能力
证明有界深度 CC-电路与同余模簇中有限幂零代数上的电路表达力等价，并联系代数版 B-S-T 猜想。
邻域框架对偶性的余代数方法
用余代数统一刻画邻域框架与邻域代数的 Jónsson-Tarski 与 Thomason 型对偶。
DA 中幺半群上的程序：Tameness 与表达能力
提出幺半群类的 Tameness 条件，证明 DA 满足该条件并刻画其程序可识别语言，同时表明 J 不满足并给出长度层级。
约束满足问题的通用代数方法
提出通用代数新方法，用于攻克小代数CSP分类难题，并证明基数≤4的交换幂等二元代数对应CSP可处理。
实数指数运算的无点构造
用无点拓扑与几何理论构造实数指数和对数，建立其代数规则并发展提升与粘合技术。
2021102 篇 · vol.Volume 17, Issue 4
高效完全高阶合一
提出高效完全高阶合一过程，通过限制搜索空间与集成片段判定，在 Zipperposition 中实现并优于已有方法。
区块链中的交易并行理论
提出基于静态分析的区块链交易并行理论，使节点并行执行交易以提升吞吐量。
计算概率自动机的概率互模拟距离
将概率互模拟距离刻画为随机博弈解，并给出首个实用的策略迭代计算算法。
针对事务性因果一致性的鲁棒性
研究事务程序对因果一致性的鲁棒性验证，并归约为顺序一致性下的状态可达性。
共归纳谓词的可表达逻辑
在共代数上为共归纳谓词建立逻辑完全刻画的一般框架，给出充分条件并实例化相似、发散与行为度量。
带经典见证的构造性Domain
提出从程序抽取视角出发、以经典正确性断言实现的构造性连续Domain理论，并给出函数空间与实数表示定理。
参数化时间自动机中的参数化更新
提出允许时钟更新为参数的时间自动机扩展，并找到一个可判定 EF-空问题、可精确参数综合的语法子类。
带单时钟与初始化时钟依赖概率的概率定时自动机
将单时钟初始化时钟依赖概率定时自动机转为区间MDP，证明其定量与定性可达性可在多项式时间求解。
双人可达性博弈的顽固集约简
提出双人可达性博弈的顽固集偏序约简理论，正确剪枝双方交错，并在TAPAAL中实现加权Petri网博弈约简。
保持 stutter 的偏序归约中不一致标记问题的详细论述
本文指出保持 stutter 的偏序归约早期 stubborn sets 条件存在错误，给出反例并提出更强条件与正确性证明。
面向 Eilenberg--Moore 代数的代数语言理论
提出基于 Eilenberg--Moore 代数的代数语言理论，支持无限多 sort 的代数并借助可定义代数连接逻辑。
Coq 中的可计算分析与连续性概念
在 Coq 中基于 Incone 库形式化可计算分析，给出连续结构上可执行算法的正确性证明。
概率高阶不动点逻辑（PHFL）
提出概率高阶不动点逻辑 PHFL，证明其表达力与模型检测的不可判定性，并用类型系统刻画可判定片段。
概率逻辑编程的余代数语义
用余代数模型为概率逻辑编程及加权逻辑编程建立语义，给出推导树与可能世界解释并恢复分布语义。
论高阶概率子递归
研究给 Gödel T 加入不同概率选择算子后的表达力，证明它们均几乎必然终止但可生成不同的分布类。
正确且高效的精化检查反链算法
指出现有反链精化检查算法的可靠性与性能缺陷，提出正确高效的新算法，实验证明其运行时间和内存更优。
在多项式空间内计算循环程序的紧多项式界
证明循环程序紧多项式界计算问题是 PSPACE 完全，并给出空间高效分析算法。
带长度约束的二次词方程、计数器系统与带整除的 Presburger 算术
通过计数器系统与带整除 Presburger 算术，给出 flat 二次词方程长度约束的可判定性与复杂度上界。
多模态依赖类型论
提出 MTT：由 mode theory 参数化的多模态依赖类型论，统一涵盖守卫递归、公理凝聚与参数量化等情形。
异步会话子类型的一种可靠算法及其实现
提出异步会话子类型的一种可靠但不完备的检查算法，并实现工具评估其适用性与开销。
数据字转换器的合成
研究无限字母表数据 ω-词上带寄存器自动机与转换器的反应式合成，给出可判定性与不可判定性边界。
使用直觉主义模态逻辑刻画开放互模拟
提出直觉主义模态逻辑 OM 刻画开放互模拟，并从完备性证明提取区分公式生成算法。
借助凸代数幂的分布双相似性
用余代数与凸代数统一刻画概率自动机的分布双相似性，并给出直到凸包的互模拟证明技术。
无量词分离逻辑的完全公理化
提出无量词分离逻辑的首个内蕴希尔伯特式完全公理化。
涉及任意实数的线性递推判定问题
为任意实数线性递推的 Skolem、Positivity 与 Ultimate Positivity 问题构造近乎可判定的部分算法。
正则余归纳的基础
为推理系统提出正则解释，统一归纳与余归纳，建立证明论与算法基础，并扩展到 corules。
乘法线性逻辑中并行切消的一个应用：证明网的 Taylor 展开
在乘法线性逻辑证明网中给出并行切消的路径约束，刻画 Taylor 展开无限和可归约的充分条件。
名义迁移系统的模态逻辑
为名义迁移系统建立 Hennessy-Milner 逻辑，证明对双模拟表达完全并机器化。
带数据的混合 XPath 的公理化
为带数据约束的混合 XPath 建立可靠且强完全的公理化系统，并研究树模型公理化与可判定性。
加权自动机的泵引理
为 min-plus、max-plus 与自然数半环上的五类加权自动机片段建立泵引理，并证明歧义层次严格。
将高阶归纳类型构造为群胚商
证明所有有限1-截断高阶归纳类型均可由群胚商构造，并在Coq中形式化。
参数化广播网络中的重构与消息丢失
给出可重构与消息丢失广播网络中覆盖性问题的 cutoff/执行长度紧界，并证明 cutoff 优化问题 NP 完全。
标记马尔可夫过程的半拉回
将标记马尔可夫过程中行为等价可构造互模拟 semipullback 的结果推广到更广的可测空间。
带数组的符号堆蕴含的可判定性
证明了带 Presburger 算术与数组的符号堆蕴含有效性检查在两个片段中可判定，并给出判定过程。
同伦类型论中的 2-伴随等价
在同伦类型论中引入（半）2-伴随等价并证明其预期性质，且在 Lean 中形式化。
无 λ 高阶逻辑的叠加演算
为无 λ 高阶逻辑提出反驳完备的叠加演算，支持部分应用和应用变量，并在 Zipperposition 中实现评估。
精确实数算术的逻辑
在 Minlog 中形式化共归纳实数流，并从证明中提取精确实数除法算法，再转译到 Haskell 运行。
无新变量的 DRAT 与传播冗余证明
无新变量时 DRAT、SPR、PR 等传播冗余证明系统的复杂度与等价性，并给出 RAT^- 指数下界。
可呈现的签名与初始语义
提出可呈现签名与初始语义框架，为带变量绑定等的语法构造提供组合式规范及机器检验的替换与归纳递归原理。
使用互模拟发现电子护照（ePassport）漏洞
用开放互模拟与经典FM模态逻辑发现并证明电子护照BAC/PACE协议的可链接性隐私漏洞。
带状态仿射向量加法系统（affine VASS）中可达性的复杂度
给出了仿射 VASS 整数可达性的复杂度三分律及标准可达性的二分律，形成统一复杂度图景。
控制随机群体
证明了随机参数化系统的控制问题是可判定的，并引入顺序流问题研究其复杂度。
自适应非线性模式匹配自动机
扩展自适应模式匹配自动机以支持非线性模式，通过交错变量一致性检查与匹配来减少匹配步骤。
嵌套类型与 GADT 的参数性
为直接以不动点构造的嵌套类型建立参数模型，推导自由定理，并揭示 GADT 扩展的局限。
公理化最大进度与离散时间
引入优先级作用域算子 pri(E)，给出带优先级与非守卫递归的基本进程代数的完备公理化，解决了用标准观测同余公理化优先级这一长期开放问题。
论 LPMLN 程序的强等价
提出 LPMLN 程序的 p-强等价并给出模型论刻画、复杂性及化简条件，系统研究其强等价性质。
卷积代数：关系卷积、广义模态与关联代数
用关系卷积统一刻画子结构/区间逻辑的广义模态与关联代数语义。
π演算具有行为完备性且轨道有限可执行
证明π演算可规范所有有限可执行行为，并在轨道有限松弛下与反应式图灵机行为等价。
输出敏感的信息流分析
提出输出敏感非干扰与类型系统，验证泄漏变量泄露不超过公开输出。
ζ(3) 无理性的形式化证明
在 Coq 中完整形式化了 Apéry 关于 ζ(3) 无理性的证明，并验证了计算机代数计算。
控制算子的完备传值调用演算 II：强终止性
本文刻画了 CCV lambda-mu 演算的强终止性，并给出其与 CPS 语义及类型可推导性的等价表征。
并发中的雕塑
形式化 Pratt 的高维自动机雕塑过程，刻画可雕塑 HDA 的表示能力并给出判定算法。
代数余完备性与有限函子
证明若干范畴代数完备且余完备，有限集合函子的初始代数与终端余代数具有相同理想CPO与Cauchy完备化。
Setoid 中的 W-类型
在 Setoid 模型中用依赖 W-类型构造 W-类型，证明 setoid 范畴有多项式自函子的初始代数，并给出 Coq 形式化。
正则与 ω-正则行为的余代数视角
在 monad 余代数框架下统一刻画有限与 ω-正则行为，并给出对应 Kleene 定理及多类自动机实例。
通过可编程分布式调度器实现时间流体式基于场的协调
提出用因果场编程分布式调度，替代固定时钟，实现可平衡反应性与开销的时间流体式场协调。
查询回答中元组的 Shapley 值
将 Shapley 值引入查询回答，量化元组对合取与聚合查询答案的贡献，并给出复杂度与近似算法。
ReLoC Reloaded：面向细粒度并发与逻辑原子性的机械化关系逻辑
提出 ReLoC 新版本，为高阶状态与细粒度并发程序提供机械化关系分离逻辑，支持精化证明与逻辑原子关系规约。
分离性（Apartness）与互模拟（Bisimulation）的关系
从余代数对偶视角关联 apartness 与互模拟，并为弱/分支互模拟建立 apartness 证明系统。
带状态整数向量加法系统的仿射扩展
研究仿射 Z-VASS 可达性，将有限矩阵幺半群情形归约到 Z-VASS，证明转移/复制变体 PSPACE 完全，并讨论单基因矩阵。
有界线性团宽度图的可定义分解
证明 MSO_1 转导可从有界线性团宽度图非确定输出有界团宽度分解，并推出 CMSO_1 可定义性与可识别性等价。
偏序自动机与分段可测试性
系统刻画偏序自动机的包含、等价与(k-)分段可测试性判定复杂度，并证明一般 ptNFA 通用性与一般 NFA 同难。
面向质量与资源管理的接口建模
提出面向质量与资源管理的接口建模框架，用偏序集统一刻画软硬件组件的功能、资源与质量工作点。
在线结构理论的基础 II：算子方法
提出在线结构理论的算子框架，统一在线算法、可计算分析、Weihrauch 归约与反推数学等。
立方类型理论的内部参数性
提出融合笛卡尔立方类型理论与内部参数性原语的计算类型理论，同时支持 univalence 与关系等价（relativity）。
离散出价无限持续时间博弈中的决定性
首次研究离散出价无限持续时间博弈，证明多数自然平局机制下该类博弈具有决定性。
范畴量子力学的 Dagger 线性逻辑
推广范畴量子力学至无限维过程，建立乘法 Dagger 线性逻辑的范畴语义并定义 mixed unitary category。
可解性 = 可类型性 + 居留性
将可解性推广到带模式匹配的 lambda 演算，并证明其恰由非幂等交类型的可类型性与居留性刻画。
LNL-FPC：线性/非线性不动点演算
提出混合线性与非线性递归类型的 LNL-FPC，并给出其范畴模型与递归域方程求解技术。
实数加法理论：带整数谓词与不带整数谓词
证明实数加法结构中有无整数谓词的可定义性可判定，并给出拓扑刻画与无中间结构结果。
序理论树中 betweenness 关系的公理化
给出序理论树中介于关系的 MSO 公理化，并证明拟树上的诱导介于关系可由一阶语句刻画。
Bishop 空间的直接谱及其极限
在 Bishop 集合论中建立 Bishop 空间直接谱、正/逆极限及对偶定理。
带超时算子的进程代数的失败迹语义
为进程代数引入超时算子并给出其失败迹语义，刻画迹等价与失败等价的同余闭包。
连续格的直谓理论
引入强邻近并半格作为直谓连续格概念，并用余代数与蕴含关系给出刻画。
笛卡尔差分范畴
提出笛卡尔差分范畴，统一笛卡尔微分范畴与变化作用模型，并涵盖有限差分与光滑微分。
dot-depth 2 的分离
为 dot-depth 2 给出分离算法，并证明基有限的拼接层级第一层分离可判定。
可逆多方协议的因果一致性
将可逆语义扩展到异步多方会话协议，并证明其回滚满足因果一致性。
Parity Exists 查询的动态复杂性
证明 parity-exists 查询无法用量词无关一阶更新规则动态维护，并揭示辅助关系元数层级与度数受限可维护性。
可达性切换博弈
系统研究零/一/二人可达性切换博弈的判定复杂度，并证明其比随机博弈版本更难。
归纳形式拓扑、Church 论题与选择公理的可实现性语义
为最小主义基础内涵层 mtt 扩展归纳形式拓扑、Church 论题与选择公理，构造 Kleene 可实现性语义并在 CZF+REA 中形式化。
带代数标量乘法的 Presburger 算术
证明将 Presburger 算术扩展为代数无理数标量乘法后，判定复杂度显著升高，非二次情形甚至不可判定。
论存在二阶逻辑的并封闭片段与带团队语义的逻辑
为存在二阶逻辑与团队语义逻辑的并封闭片段给出句法刻画，并引入包含-排斥博弈及新原子。
弱双 Kleene 代数的等价性检查
刻画了 pomset 自动机中语言等价可判定的片段，并证明其恰对应系列有理表达式。
有界度类上的后继不变一阶逻辑
证明在有界度结构类上，后继不变一阶逻辑的表达能力不超过普通一阶逻辑。
完全选择公理的一个程序
在经典可实现性框架下，首次给出对应于完全选择公理（AC）的显式程序。
通过一阶迁移系统实现高阶语言的模块化 up-to 共归纳
将一阶 LTS 的 up-to 双模拟理论经全抽象翻译迁移到高阶语言，实现模块化共归纳证明。
正则无限树语言的歧义层级
证明正则无限树语言在歧义度上形成严格层级，从k歧义到有限、可数、不可数歧义逐级分离。
论满足 CMSO 性质的母图
给出构造性元定理，可在参数化时间内判定图是否存在满足 CMSO 性质且有界树宽的母图，并用于图补全问题。
事件结构中依赖关系的一种新的操作式表示
为上下文相关事件结构提出相应的 Petri 网表示，用上下文弧操作式刻画依赖关系。
Stashing 与并行化五边形
引入与并行化对偶的 stashing 操作，证明其在 Weihrauch 格中至多产生五类度数并形成五边形，并刻画不连续问题。
参数化基于构件系统中的体系结构：定性与定量建模
提出参数化构件系统的扩展交互逻辑及其加权版本，证明关键判定问题可判定。
最小不动点逻辑中的驯顺性与 McColm 猜想
研究最小不动点逻辑的四种模型论驯顺性，证明其仅依赖一阶极限理论，并在驯顺极限理论下证实 McColm 猜想。
自然数与整数的数据类型定义重写系统
提出并证明自然数与整数算术的数据类型定义重写系统（DDRS），覆盖一元、二进制和十进制视图的 ground-complete 重写规则。
星游戏与九头蛇
提出星游戏，用树上的简单规则直接证明重写终止性，并给出 Hydra 战斗的无序数证明。
在 λ-演算中编码多值逻辑
将 Church 布尔编码推广到无穷 λ-演算，用 ⊥ 标识不可解项，从而编码 McCarthy 三值逻辑并可细化到四、五值逻辑。
表示索引容器的最大不动点之间的连续函数
将余归纳类型间的可计算函数表示为类型论中的特殊 transducer，推广流函数工作并在 Agda 中形式化。
带算术的模块化路径查询
提出支持算术与最小/最大路径性质的模块化图数据库路径查询形式，并证明查询可在非确定性对数空间内回答。
模态函数式（Dialectica）解释
将轻量 Dialectica 解释扩展到模态公式，并证明其对基于 Gödel T 与经典 S4 的非标准模态算术可靠。
有界与无界非确定性的外延语义与内涵语义
用双序与有序具体数据结构上的非确定顺序算法，统一刻画有界与无界非确定性的外延/内涵语义，并分析 may/must 测试的完全抽象性。
超图分离定理与一个 CSP-SAT 算法
证明超图分离定理，并据此给出变量频率受限 CSP 的亚指数时间 SAT、#SAT、MaxSAT 算法及 resolution 反驳。
论 p/q-可识别集合
研究有理数基 p/q 的可识别集合：给出一阶逻辑刻画，并证明自然序与模 q 运算不可识别。
异步消息传递模型的 Heard-Of 谓词刻画与推导
证明可用 Heard-Of 谓词刻画异步消息传递模型，并给出经 delivered 谓词的两步推导框架与轮次切换策略。
202084 篇 · vol.Volume 16, Issue 4
论核心：马尔可夫决策过程的部分探索框架
提出 MDP 部分探索框架，通过识别高概率核心并给出严格误差界，高效近似分析多种时域性质。
循环程序的紧多项式最坏情况界
为带界循环的非确定性命令式程序提出算法，自动求出渐近紧的多变量析取多项式最坏情况界。
高效且模块化的余代数划分细化
提出通用余代数划分细化算法，按行为等价商化系统，复杂度 O(m log n)，并统一多种系统类型。
基于 Riesz 空间的概率逻辑
提出 Riesz 模态逻辑，用 Riesz 空间建立概率转移系统性质的对偶理论，并给出可靠完备公理化与概率互模拟刻画。
生命是随机的，时间不是：具有窗口目标的马尔可夫决策过程
将窗口机制扩展到马尔可夫决策过程，解决窗口目标的阈值概率问题并给出通用策略综合方法。
状态之间与谓词之间的距离
借助有效关系统一刻画概率状态与谓词上的度量，并应用于经典和量子概率的 state-and-effect 三角。
高阶解释理论及其在 Basic Feasible Functions 中的应用
将解释方法扩展到纯高阶函数式语言，并用高阶多项式刻画任意阶 Basic Feasible Functions。
概率 call-by-name FPC 中的凸性与序
证明 Kegelspitzen 构成概率 call-by-name FPC/pPCF 的指称模型，并讨论概率递归类型解释。
一种建立服务级别协议的对称协议
提出一种双方动态协商服务等级的对称协议，并用模态公式与行为归约验证其正确性。
概率高阶递归程序的终止性问题
提出PHORS模型，证明二阶几乎必然终止不可判定，并给出终止概率的不动点刻画与近似算法。
参数化时间自动机中的语言保持问题
证明参数化时间自动机的无时间语言与迹保持问题一般不可判定，并给出若干可判定子类及鲁棒变体。
论循环算术的逻辑复杂度
证明循环算术 CΣ_n 与 IΣ_{n+1} 的 Π_{n+1} 定理相同，并给出证明规模与一致性强度新界。
自动机最小化：一种函子式方法
用函子与伴随刻画自动机及其最小化，统一确定化、最小化与句法代数。
充实范畴论中的经典控制、量子电路与线性逻辑
用充实范畴为基于电路的量子函数式语言建立范畴语义，并连接线性/非线性模型。
Coaxioms：通过推理系统实现灵活的共同归纳定义
提出 coaxioms 推广推理系统，使递归定义可解释为既非最小也非最大的不动点。
高阶归纳-归纳类型的签名与归纳原理
提出 HIIT 签名的类型理论，统一描述高阶归纳-归纳类型，并通过语法逻辑关系翻译计算归纳/递归原理。
迈向最小稳定子 ZX 演算
证明稳定子 ZX 演算多数重写规则必要，仅两条必要性待定；并表明辫式自治范畴足以恢复“仅连通性重要”元规则。
将离散函数的算法描述翻译为 SAT 及其在密码分析问题中的应用
提出将离散函数算法描述归约为 SAT 的技术与 Transalg 工具，用于代数密码分析并构造攻击。
非正曲率空间中的有向同伦
本文用预立方集合为互斥锁并发程序建模，引入非正曲率概念，证明有向同伦与无向同伦在特定有向路径上一致。
带证明无关命题等式的非直谓类型论中归一化失败
构造反例证明带证明无关命题等式的非直谓类型论不满足归一化，反驳 Werner 猜想。
电路下界与有界理论的一致性
证明若干有界算术理论无法证明对应复杂度类具有无限频繁的电路上界，即电路下界与这些理论相容。
自然演绎风格经典演算的非幂等类型
为λμ演算引入非幂等交并类型系统，用类型推导刻画头/强归一化并给出归约长度上界，并扩展至小步λμs演算。
传名调用的渐进类型论
提出传名调用渐进类型论，用泛性质刻画动态类型、类型转换与类型错误，并由渐进保证唯一确定转换行为。
无穷 lambda 演算中一种新的余归纳合流性证明
提出无穷 lambda 演算中 Böhm 归约合流性与规范化的新余归纳证明，并在 Coq 中形式化。
迈向线性逻辑中的竞态
将非确定性引入基于线性逻辑的 HCP 进程演算，在保持无死锁性的同时刻画竞态与选择。
带标签马尔可夫决策过程中的迹精化
研究了带标签 MDP 间迹精化问题的可判定性，证明第二 MDP 为马尔可夫链时多项式时间可判定，一般情形不可判定。
位置/变迁 Petri 网的可逆化
为 P/T Petri 网提出基于展开的因果可逆语义，并用带因果历史颜色的有限网表示其可逆行为。
可见下推自动机的最小化是 NP 完全的
证明可见下推自动机最小化问题是 NP 完全的，并借助 immersions 给出归约。
编排与协同的综合：弥合监督控制与服务协调之间的鸿沟
提出新可控性概念，将监督控制的经典综合改造为服务合约自动机的编排与协同综合，并给出统一抽象算法。
良结构迁移系统的前向分析，第三部分：Karp-Miller 树
为 very-WSTS 提出通用 Karp-Miller 算法，可计算覆盖集并判定 LTL 模型检测。
平坦 FIFO 系统的验证
证明平坦 FIFO 机及其有损/前端有损变体的多类验证问题为 NP 完全，并给出可模型检测的等价系统构造。
构造性分析中的 McShane-Whitney 扩张
在 Bishop 式构造性数学中建立 McShane-Whitney 扩张，给出 Lipschitz 函数稠密性及 Hölder/ν-连续扩张。
论名义语法与置换不动点
提出基于置换不动点约束的名义项 α-等价公理化，并建立新的名义合一及 C 理论下的有穷性结果。
定性约束满足问题组合的复杂度
证明在一大类 ω-范畴理论中，Nelson-Oppen 组合条件对并集 CSP 的多项式时间可解性也是必要的（除非 P=NP）。
BPMN 中协作与编排的一致性
提出 BPMN 编排图与协作图的操作语义及两种一致性关系，并实现工具 C4 支持实践验证。
重叠代数：构造性地审视完全布尔代数
研究重叠代数范畴，将其视为集合与关系范畴的扩展，并建立与完全布尔代数及 locale 的构造性联系。
T-可定义泛函连续性的语法方法
用 System T 自翻译、连续性谓词和参数化逻辑关系，给出 T-可定义泛函连续性的新语法证明并在 Agda 中形式化。
唯一完美匹配、禁止转移与带 Mix 的线性逻辑证明网
该文将 MLL+Mix 证明网正确性归约为完美匹配唯一性，并由此给出线性时间判定与准线性顺序化算法。
用于合流性与交换性的递减图
研究递减图标签数对合流证明力的影响，证明两标签足以处理共终系统，并揭示交换性层级不塌缩。
子句集环与归纳
将饱和证明器中基于循环检测的归纳证明方法抽象为子句集环，并厘清其与若干归纳理论的包含关系。
递归方案、MSO 逻辑与 U 量词
证明了带受限 U 量词的 MSO 逻辑对递归方案生成树的模型检测可判定，并给出反射与有效选择性质。
事件结构中依赖关系的表示
提出以修饰符决定的上下文为核心的事件结构，通过上下文与依赖事件集重新定义配置，并统一多数已有事件结构模型。
弱版本 MSO+U 的不可判定性
证明 MSO 在 ω-词上加谓词 U1 后与 MSO+U 等表达力因而不可判定，并推出最终周期集合量化亦不可判定。
论 B-项的性质
研究仅由 B 组合子构成的 B-项在重复右应用下是否循环，给出等式公理化与检测循环的规范表示算法。
在近似介值定理的两种选择之间插值
构造性证明近似介值定理：仅需逐点连续，避免可数选择与有理逼近表示。
高阶类型中连续性与复杂性的统一框架
提出参数化单子翻译，统一刻画高阶计算中的终止性、连续性与复杂性。
一个带有 λ 类型化 λ 表达式的扩展类型系统
提出扩展类型系统 d，以 λ 类型化 λ 表达式统一处理证明与公式，并证明其归一化与一致性。
不动点组合子作为高阶不动点生成器的不动点
研究弱不动点组合子生成器的结构，给出其不动点存在的充分条件并提出弱常性必要性猜想。
论高阶下推系统的表达能力
证明二阶确定性可坍缩下推自动机严格强于任意阶无坍缩确定性高阶下推自动机，并给出相应树/递归方案分离。
同伦类型论中的胞腔上同调
在同伦类型论中发展胞腔上同调，并在 Agda 中形式化其对有限胞腔复形的计算能力。
论编排中非确定性的消解
提出 whole-spectrum implementation 可实现性概念与类型系统，刻画编排中非确定选择如何由确定性实现完整实现。
无限树的函数式（一元）二阶理论
为无限树上的 MSO 给出完备公理化，并引入表达能力更强的 FSO 以证明 Rabin 树定理。
共归纳类型的操作解释
为严格正嵌套高阶（共）归纳类型提出基于重写的操作语义，用极限刻画无限归约并给出类型正确性准则。
同伦类型论中的模态
系统建立同伦类型论中的因子分解系统、反射子宇宙与模态理论，并用局部化高阶归纳类型构造它们。
ZX-Calculus 的完备性
为 ZX-Calculus 建立 Clifford+T 乃至无限制片段的完备公理化，并给出简化版本。
模态逻辑的双上下文演算
为 K、T、K4、GL、S4 的必要性片段建立双上下文自然演绎与模态 λ 演算，并给出范畴语义。
归纳不等式的构造性典范性
在构造性元理论中证明归纳不等式对正规/正则格扩张簇的典范性，推广了 Sahlqvist 结果的构造性版本。
定量可达性博弈中子博弈完美均衡的复杂度
证明定量可达性博弈中 SPE 约束存在问题是 PSPACE 完全的，并给出约束不动点算法。
一个通用的常微分方程
证明存在固定多项式 ODE，通过选择初始条件可逼近任意正连续函数，并解决 Rubel 唯一解公开问题。
从 Taylor 展开重新审视按值调用 Böhm 树
为按值调用 λ 演算引入置换规则，建立 Böhm 树与程序近似理论，并用 Taylor 展开刻画观测等价。
量子理论的范畴论重构
从范畴公理重构有限维量子理论，证明其等价于环 S 上的广义量子理论，且无需层析假设。
计数复杂性类的描述复杂性
提出基于加权逻辑的 QSO，统一刻画 FP、#P、FPSPACE 等计数复杂性类并引入 #P 内层级。
Adhesive 范畴上的规则代数
证明 DPO 重写规则的序贯复合在 M-adhesive 范畴中具有结合性，并定义规则代数及其典范表示。
随机重写系统的组合转换与矩互模拟
提出组合转换与矩互模拟，将随机重写系统动力学与规则代数及化学反应分析技术联系起来。
使用 Share 算子的基于场的协调
提出 share 算子统一场计算的时空操作，可替代 rep/nbr 并显著加速自稳定算法。
滴答时钟作为依赖右伴随：时钟类型理论的指称语义
为 CloTT 给出指称语义，用依赖右伴随在切片范畴中建模时钟滴答，并修复此前有缺陷的模型。
带有若干 betweenness 关系的二变量逻辑：表达力、可满足性与成员性
研究在有限词上加入 a 或因子 u 介于两位置之间的二变量逻辑，刻画表达力、可满足性复杂度与代数成员判定。
用经典连接词进行编译
将极性扩展到 call-by-need 并引入四种对偶移位，用经典连接词编码类型以编译惰性函数语言。
正则树代数
引入正则树语言识别器的一类代数，证明其唯一构成伪簇并构造句法代数。
寄存器博弈
提出寄存器博弈，为 parity game 给出新的准多项式时间算法，并改进交替奇偶自动机翻译与层级结果。
连续正则函数
证明连续 r-正则函数在无处稠密闭零集外局部仿射，且可微 r-正则函数必为仿射，并给出 PSPACE 判定。
超限 Lyndon 词
将 Lyndon 词推广到超限词，证明在稠密非增条件下存在唯一 Lyndon 分解，并刻画有理词的分解形式。
函数性转换器的连续性：有理函数的 profinite 研究
研究函数性转换器相对于正则语言类的连续性判定，建立 profinite 代数理论并比较两种代数方法。
论开放良滤空间
引入开放良滤空间，证明核紧开放良滤空间是sober的，从而解决Jia-Jung公开问题。
利用能量游戏处理数据词中的重复
该论文将数据词上重复值逻辑的博弈问题与能量游戏及带状态向量加法系统联系起来，并给出可判定片段。
有根发散保持分支互模拟是同余关系
证明在由 nil、动作前缀、选择与递归构成的过程语言中，有根发散保持分支互模拟是同余关系。
Psi-calculi 再探：连通性与组合性
提出带 provenance 标注的新操作语义，解除 psi-calculi 对信道对称传递的限制并保持双相似代数性质。
KPT 插值的一个局限性
证明 Pich 和 Santhanam 提出的 KPT 插值变体对一类能证明难以区分的 NP 集合不相交的命题证明系统存在局限。
线性序上的点与区间统一一阶理论（第二部分）
对线性序上的点-区间两类一阶语言进行相对表达力完全分类，并确定其本质不同的扩展。
长纸带无限时间图灵机的可达性
确定长纸带无限时间图灵机中最小不可达停机位置的序数 δ，并给出多个序数刻画。
Scott 可实现性拓扑斯中的 Sierpinski 对象
研究 Scott 可实现性拓扑斯中的 Sierpinski 对象 Σ，刻画序离散对象、dominance 与同伦模型。
Corrado Böhm 的珍宝
综述 Corrado Böhm 在自编译编译器、结构化编程、函数式编程与 λ 演算等方面的奠基性思想。
有界扩张结构类上的一阶查询
重新证明有界扩张结构类上一阶查询可线性时间求值，并实现常延迟枚举与线性时间计数。
论可计算维数的不可计算性
通过迭代树构造证明，康托尔空间中简单可计算子集的豪斯多夫维数、构造性维数和可计算维数都可能不可计算。
2019105 篇 · vol.Volume 15, Issue 1
非确定性自动机的高效约简及其在语言包含测试中的应用
提出高效的 NFA/NBA 约简算法，并显著扩展语言包含等 PSPACE 完全问题的可解规模。
全路径可达性逻辑
提出语言无关的全路径可达性逻辑，以操作语义为公理证明非确定性程序的部分正确性。
几乎每个简单类型 λ 项都有长的 β-归约序列
证明在函数元数与变量数有界时，渐近几乎所有 k 阶简单类型 λ 项都有长达 (k-1) 重指数的 β-归约序列。
论缓存算法在时序泄漏方面的不可比性
提出 leak competitiveness 比较缓存算法时序泄漏，证明算法间无泄漏支配关系，有限控制下关系仅线性或常数。
SPARC TSO 的一种指称语义
为 SPARC TSO 弱内存模型提出可组合的 pomsets 指称语义，并证明其相对公理语义可靠且完备。
概率语义下的定量自动机
证明 monitor counter 自动机与嵌套加权自动机等价，并刻画其在概率语义下的可判定性与复杂度。
用于检查归纳不变式的有界量词实例化
提出有界视界量词实例化，使 SMT 检查归纳不变式终止，并证明其至少等价于手工 instrumentation。
抽象隐马尔可夫模型：定量信息流的单子式刻画
用 Giry 单子与抽象 HMM 为隐藏状态概率程序建立信息流语义、安全序与不确定性变换。
关于效应的推理：从列表到信息物理智能体
回顾从列表、高阶函数、Actor 到信息物理智能体的效应推理发展，总结核心原理并展望未来挑战。
实时能量问题的 ω-代数
提出实时能量函数的 *-连续 Kleene ω-代数，并据此静态判定实时能量自动机的可达性与 Büchi 接受性。
超越 MSO 的简化算法元定理：树宽与邻域多样性
研究 MSO 扩展在树宽与邻域多样性图上的模型检测复杂度，给出 FPT/XP 算法与 CSP 归约方法。
论幂空间（powerspace）构造的可交换性
证明 quasi-Polish 空间上上下幂空间可交换，等价于 consonance，并刻画其对开集格构造的分配。
概率化的 Call-By-Push-Value
在概率相干空间模型中为 Call-By-Push-Value 加入随机选择，并证明其可靠性与完全抽象。
论 Thin-Air Reads：迈向松弛内存的事件结构模型
用带证成关系的无混淆事件结构建模松弛内存，提出良证成配置以排除 thin-air reads，并证明 DRF 与 rely-guarantee 可靠性。
Martin-Löf 归纳定义的经典系统与循环证明不等价
证明含 Martin-Löf 归纳定义的经典系统 LKID 与循环证明系统 CLKID-omega 并不等价。
嵌套词转导的可流式性
研究可见下推转换器定义的嵌套词转导能否单遍流式求值，给出 HBM 判定与二次内存充分条件。
多项式常微分方程中的代数、余代数与最小化
用Lie导数上的L-双模拟刻画多项式ODE的解等价，并给出最小化约简算法。
大小、成本与容量：面向难随机 QBF 的一种语义技术
提出基于成本与容量的语义技术，为多个 QBF 证明系统证明指数级下界，包括随机 QBF。
规范模型与模态团队逻辑的复杂度
引入规范模型方法，将MTL可满足性归约为模型检测，并证明其完全性位于TOWER(poly)。
Shrub-depth：捕捉稠密图的高度
综述 shrub-depth 的定义与性质，并用其刻画简单图 MSO1 转导层级的前 ω 层。
展示范畴
提出展示范畴概念，将纤维化等范畴构造从对象相等中解放，并在 Coq/UniMath 中形式化。
一计数器系统中的最短路径
证明 n 状态一计数器自动机非空语言存在 O(n^2) 长度接受词，并给出配置间最短路径的紧上界。
递归的轻量模态
提出静默模态与守卫递归类型的 Curry 式 λ 演算，由编译器控制递归，保证归一化并支持类型推断。
论度量时序逻辑的表达力与监控
扩展 MTL 使其在有界及允许有理常数的无界 timed words 上与 FO[<,+1] 等表达力，并给出迹长无关监控。
Church 合成问题的 Curry-Howard 方法
引入无穷字上 MSO 的直觉主义变体 SMSO，通过基于自动机的可实现性模型建立其与 Church 合成的可靠性与完备性。
自然变换作为重写规则与 Monad 复合
用字符串重写与合流性刻画 monad 与伴随，简化 monad 复合验证。
论诱导子图同构的一阶复杂度
研究诱导子图同构的一阶变量数 W[F]，给出 paw 图等精确值与一般下界，并导出单子二阶逻辑简洁性结果。
带权奇偶博弈
研究带任意整数权重的奇偶博弈，证明求解属于 NP ∩ coNP，给出策略内存与质量的紧界，并证明阈值问题 EXPTIME 完全。
将集合函子扩展为广义度量空间
证明集合自函子可典范扩展为广义度量空间上的自函子，并用左 Kan 扩展计算实例与终余代数。
证明外延正规形式互模拟的可靠性
提出一套系统化方法，用于证明带 η-展开的外延正规形式互模拟及其 up-to context 技术的可靠性。
Companion、因果性与余密度
把共归纳 companion 提升到 universal coalgebra，证明 final distributive law 是 codensity monad，并用因果性刻画 up-to 技术。
可判定不动点逻辑中的可定义性与插值
研究守卫等可判定不动点逻辑中公式可定义性与插值，通过树模型性质及关系/树逻辑转换给出语义与有效刻画。
计算非确定性自动机的宽度
提出自动机宽度度量以量化非确定性，并研究其确定化与计算复杂度。
概率蕴涵之间的相对蕴涵
用线性规划对偶精确刻画任意多前提的概率蕴涵及相对蕴涵，并给出更优判定算法与临界置信阈值。
分离逻辑的 Stone 型对偶性
系统建立束逻辑与分离逻辑的 Stone 型对偶，统一代数/关系/拓扑语义并推出可靠完备性。
表示空间的 Moschovakis 扩展
为表示空间的 Moschovakis 扩展构造表示，并证明 TTE 可计算性下若干单值/多值函数定理。
Wadge 层级低层中的正则树语言
给出正则无限树语言在 Wadge 层级低层的有效刻画，并证明相应成员性可判定。
用高维自动机建模共享变量系统
提出用高维自动机组合式建模共享变量系统的构造，其中并行组合对应张量积、非确定性选择对应余积。
并发与概率：组合式消除混淆
提出基于结构分支单元的组合式方法，将含混淆的 Petri 网转换为无混淆网，从而为分布式选择赋予概率语义。
归约规则的初始语义
用范畴模型初始对象统一刻画带变量绑定的简单类型语法及其归约规则，并构造保持归约语义的翻译。
有限域上组合猜想的计算机辅助证明：一个国际象棋猜想案例研究
用机器可验证方法证明 n×n 棋盘扩展 KRK 残局白方必胜，并展示多种计算机证明方法的协同。
量子网络的经典 groupoid 模型
提出基于 groupoid 的 groubit，为一种经典网络架构建模，使其可直接执行若干通常属于量子网络的协议。
定界控制算子的互模拟
为带 shift/reset 的无类型 λ 演算定义上下文等价，并在统一框架中用多种互模拟刻画其行为理论。
一种被遗忘的证明理论？
从组合逻辑视角重新审视 MacLane 的证明论论文，提示一种被遗忘的证明理论。
抽象完成的形式化
在 Isabelle/HOL 中形式化抽象完成、有序完成与 Métivier 正则性结果，并给出新的正确性证明。
Flat Freeze LTL 的复杂度
证明 flat freeze LTL 在单计数器自动机上的模型检测是 NEXPTIME-完全，统一一元与二进制编码。
面向差分隐私的关系 ⋆-提升
提出存在式 ⋆-lifting，统一近似 lifting 概念，并证明其与 Sato 构造在离散概率测度下等价。
一元析取 Datalog、MMSNP 与表达性描述逻辑中的可重写性
研究一元析取 Datalog、MMSNP 与 ALC 本体查询到 FO、MDLog、Datalog 的可重写性，给出可判定性与复杂度。
经由翻译的 Sahlqvist 理论
提出基于序理论的 Gödel–McKinsey–Tarski 翻译统一视角，并证明归纳不等式对应性与部分可典范性的迁移。
带封闭谓词的本体中介查询的数据复杂度
对带封闭谓词的本体中介查询进行数据复杂度分类，在DL-Lite、EL与ALCHI中建立可处理与不可处理边界。
Frobenius 伪幺半群的相干性与线性证明的几何
证明 Frobenius 伪幺半群与 snakeorator 的相干性，并由此给出非对称乘法线性逻辑证明的三维几何记法。
因果结构的范畴语义
提出因果结构的范畴语义框架，在过程理论中统一描述有定与不定因果序。
发散性与方程的唯一解
将CSP中基于方程唯一解的双相似证明方法迁移到CCS等操作语义，并区分发散、推广到迹等价与π演算。
带立方项的有限代数的子幂成员问题
证明在剩余小簇中，带立方项的有限代数集合的子幂成员问题是多项式时间可判定的。
带对称性的薄博弈与并发 Hyland-Ong 博弈
基于事件结构构造笛卡尔闭范畴 Cho，为高阶有状态并发程序给出精确且可组合的博弈语义。
交互图：指数连接词
本文将交互几何扩展到指数连接词，使用 graphings 为带二阶量化的初等线性逻辑 ELL 构造 GoI 模型。
Büchi 可判定性定理的逻辑强度
在 RCA0 上证明 Büchi 可判定性相关定理与 Σ^0_2 归纳、加性 Ramsey 定理等价，并蕴含 McNaughton 确定化。
论线性逻辑的非交换扩展
为半交换乘法线性逻辑建立证明网与带装饰矢列演算，并给出 Pomset 逻辑的矢列演算变体。
动态 GoI 机：一种令牌引导的图重写器
提出结合令牌传递与图重写的动态 GoI 抽象机，统一实现并分析多种 lambda 求值策略的时空效率。
Weihrauch 度中的游戏刻画与下锥
引入参数化 Wadge 游戏，刻画 Weihrauch 度的每个下锥，并统一已有多种游戏。
Böhm 树理论中的外延性程度与 Sallé 猜想
证明 B-ω 与 Morris 理论 H+ 相等，推翻 Sallé 猜想，并给出 Böhm 树外延性等价的分类。
拓扑 Scott 收敛定理
在 T0 空间框架下研究 Scott 收敛的拓扑化，并给出 I-收敛结构成为拓扑收敛的必要与充分条件。
论可由下推 Petri 网及相关系统弱计算的函数
证明语法控制向量加法系统（GVAS）能弱计算所有快速增长函数 F_α（α<ω^ω），但不能弱计算反函数或任何次线性函数。
广义 Mermin 型非局域性论证
将 GHZ 态上的 Mermin 型非局域性论证推广到一般情形，给出精确群论条件，并扩展量子秘密共享协议。
在弦无爪图上捕获对数空间与多项式时间
证明弦无爪图类具有LREC_=可定义的正则化，由此得到对数空间同构测试并捕获对数空间与多项式时间。
控制一个种群
提出种群控制问题：同一控制器对所有有限状态个体施加相同动作，能否在任意个体非确定性反应下同步驱动任意数量个体到目标状态。
Timed 系统的行为等价关系
首次提出统一的 timed 行为模型框架，将各种 timed 行为等价按区分力统一为谱系。
模态与命题依赖逻辑中的有效性与蕴涵
系统刻画模态与命题依赖逻辑中有效性与蕴涵问题的复杂度，并证明模态依赖逻辑有效性为 NEXPTIME 完全。
动态程序的一种策略：重新开始并勉强推进
提出构造 DynFO 动态程序的“重算+有限步维护”策略，将 AC^1 初始化后 log n 步能力化为 DynFO。
一阶逻辑中图区分的量词深度上界
证明2-WL稳定需O(n^2/log n)次迭代，将C3区分n点图的量词深度上界改进至同阶。
广义过程的守卫与非守卫迭代
提出抽象守卫性统一守卫迭代与 Elgot 单子，并证明 Elgot 单子恰为抽象守卫迭代单子的迭代同余收缩。
小可加类随机图的逻辑性质
证明MSO在若干连通图类上满足零一律，去掉连通性后收敛律仍成立。
非确定性 λ-项 Taylor 展开的归一化：基于资源向量的并行归约
将 Taylor 展开与归一化交换的经典结果推广到代数 λ-演算，并引入资源向量并行归约证明该性质。
论依赖原子的简洁性
系统比较命题团队逻辑中各类依赖原子在存在片段与全片段下的简洁性，给出指数下界与多项式上界。
多项式时间内的派生 ω-树语言查询学习
首次给出多项式时间算法，用成员与等价查询学习一类非平凡的派生 ω-树语言。
费米子量子线路的图解演算
提出费米子ZW演算，为费米子量子计算提供图解语言，并证明其等式公理化完备。
Nash 均衡与互模拟不变性
揭示标准策略模型下互模拟不保持Nash均衡，并提出三种保持Nash均衡的策略模型。
名义进程演算的规则格式
提出名义剩余迁移系统及其规则格式，保证其对应名义迁移系统，并应用于π演算。
ℵ1 与模态 μ-演算
证明模态 μ-演算的连续性片段仅有 ℵ0 与 ℵ1 两类，并刻画闭包序数。
半结合律的相继式演算
提出一个限制 Lambek 积规则的相继式演算，精确刻画 Tamari 序，并证明聚焦性与唯一聚焦推导的相干定理。
Web 空间与 Worldwide Web 空间：域理论的拓扑面向
给出 web、wide web 与 worldwide web 空间及 patch 空间的新刻画，并联系连续域、Scott 空间与 fan 空间。
带模数谓词的逻辑片段的覆盖与分离
证明含后继谓词的逻辑片段在加入模数谓词后，其覆盖与分离问题可归约到原逻辑。
初等商完成、Church 论题与分划装配
把有效 topos 与装配拟 topos 都看作基于分划装配的 Lawvere doctrine 的初等商完成，以解释两种 Church 论题差异。
一种使用 LSDF 约定判定 b-可识别集周期性的高效算法
刻画周期 b-可识别集的最小自动机，并在线性时间验证，从而以 O(b log n) 判定周期性。
可定义同构问题
证明带原子可定义关系结构的可定义同构问题可判定，核心是参数消除。
有理转换的逻辑与代数刻画
将非周期语言的可判定性推广到有理转换，证明可判定转换是否属于给定同余类，并得一阶可定义性 PSPACE-完全。
基于 Moore 路径的类型论模型
提出基于 Moore 路径的内涵 Martin-Löf 类型论模型，构造非截断模型且无需 Kan 填充条件。
利用模分解捕获多项式时间
提出模分解定理，将图类可定义规范化归约到素图，并证明带计数的固定点逻辑在置换图上捕获多项式时间。
Cantor 空间上的反馈可计算性
引入 Cantor 空间上的反馈可计算函数，证明其恰为有效 Borel 函数，并将概念推广到结构上。
与词或树自动机相关的一些拓扑的 Polish 性
证明 Büchi 拓扑与 automatic 拓扑是 Polish 的，并证明在无限标记二叉树空间上 Büchi 与 Muller 拓扑不是 Polish 的。
在函数可实现性中每个度量空间都是可分的
证明在函数可实现性拓扑斯中所有度量空间可分、可判等对象可数，从而给出直觉主义逻辑不可证明相关命题的模型。
单计数器自动机的正则可分离性
证明无零测试单计数器自动机的正则可分离性可判定且 PSpace 完全，并证明带零测试时不可判定。
子空间不变的 AC$^0$ 公式
证明了 P-不变 AC$^0$ 公式计算 PARITY 的近乎匹配下界，并推广到一般子空间不变布尔函数。
交替、私有交替与量子交替实时自动机
证明了实时交替、私有交替与量子交替自动机的空问题不可判定性及若干非正则识别能力。
GPAC 中的可逼近性
扩展 GPAC，加入极限模块与流通道，使其能捕获 gamma 和 zeta 等非微分代数函数。
有界变量一阶逻辑模型检测的参数化空间复杂度
刻画有界变量一阶查询参数化模型检测的空间复杂度，证明其按量词交替秩对树层级完备，并联系 Savitch 定理。
论自由 ω-连续与正则有序代数
用 Σ-余项单子的子单子刻画准正则有序代数簇的自由代数，并给出 ω-连续与正则有序代数自由代数的关系。
论 System F 可实现性语义中的完备性与参数性
统一刻画 System F 的一类可实现性语义，证明正类型完备性及闭实现子的参数性条件。
带原子的标量与向量 μ-演算
研究带原子的模态 μ-演算扩展：轨道有限结构上模型检测可判定且对应奇偶博弈，但可满足性不可判定。
将余代数模态和 MELL 模型结构提升到 Eilenberg-Moore 范畴
证明线性范畴结构可提升到 MELL 提升单子的 Eilenberg-Moore 代数范畴，并给出由余代数群诱导提升单子的来源。
流逻辑
提出流逻辑 BFL*，将流函数作为一阶对象刻画流网络性质，并系统分析其模型检测复杂度。
分段可测试语言的高度与子词逻辑的复杂度
系统研究分段可测试语言的高度，并据此证明子词序上的二变量一阶逻辑仅能表达分段可测试性质且具初等复杂度。
无点连续性原则
在构造性无点拓扑中提出无点连续性原则，用基间关系诱导连续操作，并联系空间性与紧致性。
无限树中存在可由按排序有限代数识别的非正则语言
构造按每个排序有限且有限生成的 ω-clone，使其识别非正则无限树语言，推翻简单有限性判定。
论闭包与环境的枚举及其在随机生成中的应用
研究 lambda 演算中普通与封闭环境和闭包的渐近计数，并用生成函数构造有效随机采样器。
201894 篇 · vol.Volume 14, Issue 3
Java 与 Lambda：一个 Featherweight 故事
提出核心演算 FJ&λ，形式化 Java 8 的 lambda、交集类型与接口默认方法，并证明类型安全与推断。
论理论扩展中的插值与符号消去
研究理论扩展中插值与符号消去的层次化方法，并推广至基理论仅有可量词消去模型完备的情形。
SMT 中带基数约束的有限集合推理
提出一种结合成员约束与基数约束的有限集合判定演算，并用图增量跟踪重叠区域。
分布凸集中的终止性
刻画凸代数单点扩张，为概率系统终止建模提供完整分类，并给出唯一函子性黑洞扩张。
余代数式无穷轨迹与 Kleisli 模拟
为 Kleisli 模拟建立余代数理论，证明其对无穷轨迹包含的可靠性，并扩展前向部分执行。
最小计算集合论中的适用数学
扩展静态逻辑框架，证明最小谓词主义无限集理论是计算性的，且足以形式化大部分科学适用数学。
三值几何归结中的包含算法
将三值几何归结的包含/匹配归约为广义约束满足，提出直接算法、SAT 编码与局部一致性过滤。
用自失效与自降级修补栅栏
为采用自失效/自降级的一致性协议建立形式语义，并给出面向安全性的最小代价栅栏插入方法。
结构化可逆流程图语言的范畴论基础：可靠性与充分性
用带 join 的逆范畴为结构化可逆流程图语言建立范畴语义，并证明其计算可靠、充分且在一定条件下等式完全抽象。
余代数行为度量
在余代数框架下统一构造行为伪度量，推广 Kantorovich/Wasserstein 度量并涵盖分支时间与线性时间语义。
Globular：面向高维重写的在线证明助手
介绍 Globular——一个用图形化界面形式化并验证高维范畴论证明的在线证明助手。
无穷重写与无穷等式逻辑的余归纳基础
提出统一的余归纳框架，用于定义并推理无穷重写与无穷等式逻辑，无需序数或度量收敛。
同步与异步通信组件的兼容性性质
基于 I/O 迁移系统研究同步与异步通信组件的兼容性，给出弱异步兼容判定准则并刻画半双工系统与死锁自由关系。
基于SOS的非确定性概率进程模态分解
提出基于结构操作语义的模态公式分解方法，并为概率互模拟与相似性建立同余格式。
带持久性的 Petri 网的事件结构
将Petri网与事件结构的关系推广到析取因果，用持久库所刻画，并构造与局部连通事件结构的核反射链。
图灵跳跃与极限之间的 Galois 连接
揭示图灵跳跃与极限可计算之间的伴随关系，并在表示空间上建立形式化 Galois 连接。
归纳定理证明逻辑基础的若干观察
建立理论模型分析自动归纳定理证明中归纳公理选取的困难，并厘清不同归纳性概念的关系。
使用树自动机分析时间系统
提出用有限树自动机分析时间系统，将时间行为编码为有界树宽的图，从而用MSO与树自动机判定性质。
一种实值模态逻辑
提出基于实数格与群运算的实值模态逻辑，给出带标签 tableau、coNEXPTIME 上界，并建立乘性片段的切消除与公理化。
带升级的条件迁移系统的余代数处理
用余代数与分配格对偶统一刻画带升级的条件迁移系统，并实例化行为等价最小化算法。
非幂等交类型的居留问题
证明非幂等交类型用于刻画可解与强规范化 lambda 项的若干赋值系统中，居留问题均可判定。
单值基础中的类型论范畴结构
在单值类型论中比较三种依赖类型论的范畴模型，并给出 Coq 形式化。
直觉主义分层图逻辑：语义与证明论
提出分层图逻辑 ILGL，建立其 Kripke/关系/代数语义与可靠完备表列系统，证明可判定性、对偶并扩展至谓词版本。
概率双相似性的博弈刻画及其在下推自动机中的应用
用双人博弈刻画概率双相似性，并据此确定概率下推自动机及其子类的可判定性与复杂度界。
马尔可夫链上互模拟距离的完备定量演绎系统
为有限标记马尔可夫链的互模拟距离给出完备定量公理化，并扩展Kleene式表示定理。
加权迁移系统中关于界的推理
提出加权迁移系统中转移权重上下界的推理方法，定义更粗互模拟，并给出模态逻辑、完全公理化与可判定性。
事件结构中的动态因果性
通过允许事件增删因果依赖，提出动态因果事件结构并比较其表达能力。
（协）关系的泛构造：范畴、幺半范畴与 PROP
将关系与协关系的语义范畴刻画为更简单范畴的余极限，统一字符串图公理化。
单计数器自动机上的平坦 Freeze LTL 模型检测
证明单计数器自动机上平坦 Freeze LTL 的模型检测可判定，并通过 Presburger 算术解决参数化等值测试的可达性问题。
lambda-mu 演算的交集类型系统
为 lambda-mu 演算建立对规约与展开不变的交集类型系统，并用滤模型证明相对续延模型的完备性及强规范化刻画。
论模态逻辑的亚命题片段
为 K、T、K4、S4 的 Horn/Krom/core 等亚命题片段建立表达力层级，并证明无 diamond 的 Horn 片段可满足性为多项式时间。
自由完备 Wasserstein 代数
为概率选择操作与 Wasserstein 距离建立定量代数公理，刻画其自由完备代数。
高效判定 ground 项重写系统的合流性与范式性质
为 ground 项重写系统给出 NFP、UNR、UNC 与 CR 的更快多项式时间判定算法。
面向加权树自动机的 pushing
提出加权树自动机的权重归一化（pushing），用于最小化与等价性测试，并显著降低等价性测试复杂度。
协商中的健全性
重新审视协商健全性判定：确定性协商为NLogSpace完全，无环弱非确定性协商多项式可解，且健全性可助分析竞态等性质。
分布式自稳定协议的自动合成
提出基于SMT的方法，从高层规约和网络拓扑自动合成分布式自稳定协议。
闭集及其上的算子：表示、可计算性与复杂度
在TTE框架下用二阶表示与参数化复杂度统一刻画闭集上并、交、投影、像与求逆等算子的复杂度。
ω₁ 处的一个幽灵
证明可数幂集函子终链在 ω₁ 处含无后继的幽灵元素，故该迁移系统非强外延，并推广至其他子函子。
仿射会话类型
将会话类型的线性约束放宽为仿射性，引入优雅错误处理并保持会话不会卡死的进展性。
含否定的高阶逻辑程序的外延语义
为含否定的高阶逻辑程序提出外延语义，定义分层与局部分层，并证明分层程序不会产生 unknown 真值。
合一与对数空间
借助基于合一的代数与线性逻辑/交互几何，给出 Logspace 与 Nlogspace 的代数刻画，并联系指针机。
有限系统上互模拟与模拟问题的复杂度
确定了树、项及有界路径宽图上互模拟与模拟问题的精确复杂度分界。
基于 SSTL 的时空性质定性与定量监控
提出信号时空逻辑 SSTL 及其布尔与定量监控算法，用于时空系统的实时验证。
论 Weihrauch 度的代数结构
在 Weihrauch 度上引入复合乘积与蕴涵，系统刻画其代数结构、分配律、理想与商。
Total Store Ordering（TSO）的 Load-Buffer 语义
提出 TSO 的 load-buffer 等价语义，简化安全性验证并支持参数化验证与高效算法。
一元结构的一阶归约的二分性
证明了一元结构一阶归约的 CSP 二分性，并给出无限域 CSP 到有限域 CSP 的多项式时间归约与可解性条件。
在拓扑斯中建模立方类型理论的公理
给出一组弱公理，刻画可在任意拓扑斯内构造基于路径的立方类型理论模型所需条件，并澄清均匀 Kan 填充。
通过保守性扩展：Sikorski 定理
为有限布尔代数在分配格范畴中内射这一断言给出构造性意义，并将 Sikorski 扩张定理转为语法保守结果。
共归纳 resumption 上的无守卫递归
证明共归纳广义 resumption monad transformer 在基效应支持无守卫迭代时构成完备 Elgot monad，并给出其泛性质刻画。
分层可计算性的 Weihrauch 完备性
提出分层可计算性框架下的 Weihrauch 完备性概念，并给出若干自然实例及命中时间算子的反例。
动力系统的直觉主义时态逻辑
提出直觉主义时态逻辑 ITL^c，证明其可判定，并表明它能表达极小性与庞加莱回归。
关系图模型的应用
研究 lambda 演算的关系图模型，证明其诱导理论有最小元，并刻画对 H+ 与 H* 完全抽象性的模型条件。
在图序中定义递归谓词
引入 capable 图结构，证明子图序等图序能定义所有算术与递归图谓词。
$n$-可置换性与线性 Datalog 蕴含对称 Datalog
证明在 $n$-可置换条件下，线性 Datalog 可解的 CSP 也可由对称 Datalog 求解，从而属于确定对数空间。
SAT相关困难推理任务在Krom片段中会变容易吗？
证明CardMinSat在Krom片段仍为Θ₂-完全，并刻画其对信念修正与溯因推理复杂度的影响。
quasi-Polish 空间中 Hurewicz 定理的一个推广
识别四个对应 T2/T1/TD/T0 的非 quasi-Polish 典范可数空间，并证明 co-analytic 子集的 Hurewicz 型二分定理。
余代数谓词逻辑的模型论与证明论
提出余代数谓词逻辑，给出若干自然类的公理化与完备性，并建立基本序列演算的句法切消去。
带测度与范畴量词的一元二阶逻辑
研究在无限字与无限树上加入基于 Baire 范畴和 Lebesgue 测度的“几乎所有”量词的一元二阶逻辑扩展。
线性逻辑中的 Taylor 展开是可逆的
证明不同 MELL 证明网具有不同 Taylor 展开，并由此导出关系模型对 MELL 的完备性。
扩展的有限单子–Lawvere 理论对应关系的富集视角
用富集范畴论重新解释任意局部有限可表示基上的有限单子与 Lawvere 理论对应，并将其归约为绝对余极限下的自由完备化。
通过近似算子研究 Domain
引入受粗糙集启发的近似算子，为 Domain 理论中的连续性、way-below 关系与 Scott 拓扑提供新刻画。
基于 Scott 闭集格的定向完备偏序集的唯一性
研究哪些 dcpo 可由其 Scott 闭子集格唯一决定，并证明拟连续 dcpo 等具有 Cσ-唯一性。
无线网络 Gossip 协议中的等式推理
提出无线传感器网络概率时间进程演算的模拟理论，并以代数定律组合式估计 gossip 协议性能。
作为进程的函数所生成的树
给出λ演算到π演算编码相对于Levy-Longo树和Böhm树可靠完备的一般条件，并应用于call-by-name编码。
通过可访问路径研究 Behaviour
刻画 Ludics 中 behaviour 的可访问路径集合，给出闭合与饱和条件，并用于显式构造由常量和乘法/加法连接词生成的行为。
PCF 的递归层级是严格的
证明在 PCF 中按类型层级限制不动点算子会形成严格递归层级，低层不动点无法定义高层不动点。
诱导索引嵌套矢列式的句法切消
通过标签矢列与索引嵌套矢列式的对应，诱导句法切消并构造新的无切演算。
模态 μ-演算的模型论：语义性质的语法刻画
为模态 μ-演算的若干语义性质给出对应语法片段，并用自动机变换证明其可判定性。
Van Kampen 余极限与路径唯一性
给出 presheaf 拓扑斯中 Van Kampen 性质的充要且可高效判定条件，并揭示其路径唯一性结构特征。
句法幺半群的范畴论方法
用对称幺半闭范畴统一推广句法幺半群，统一句法代数变体，并联系最小自动机与正则语言。
分层集合语言具有合流性与强规范化性
证明分层集合语言的语法构成名义代数，且分层性/可分层性蕴含相应于β-转换的重写的合流与强规范化。
基础量子力学中的可计算性
在 Weihrauch 类型二效应性下，为量子力学基本数据结构建立可计算性，并证明有效版 von Neumann 谱定理。
覆盖问题
提出“覆盖问题”作为替代成员问题的统一框架，用于刻画正则语言的逻辑可定义性。
有限行为的 proper 函子与不动点
引入 proper functor，证明其理性不动点是终结余代数的子余代数，用于余代数正则表达式演算的可靠性/完备性。
SAT 中的局部冗余：阻塞子句的推广
提出比阻塞子句更一般的语义局部冗余性质，并证明其为最一般的局部冗余性质。
单子的 Codensity 提升及其对偶
提出 codensity lifting，将底范畴上的单子提升到纤维化全范畴，并给出对偶与代数操作提升。
双向词转换器的单向可定义性
证明双向词转换器的单向可定义性可判定，给出双指数空间算法，并可构造等价单向转换器。
Ho–Zhao 问题
否定 Ho–Zhao 问题：证明 dcpo 范畴并非 Γ-faithful，并引入涵盖已知情形的 Γ-faithful dcpo 子范畴。
效应子类型一致性的逻辑关系
提出异构双正交步进索引逻辑关系，证明效应子类型下强制语义的一致性，并机器化验证选择性 CPS 翻译。
DFA 族作为 ω-正则语言的接受器
研究 FDFA 作为 ω-正则语言接受器的复杂度：布尔运算与判定问题可在 NLOGSPACE 完成，并给出与 ω-自动机的翻译及简洁性比较。
基于交集类型的 Mixin 组合合成
提出用交集类型居留合成 Mixin 组合，并将带记录与合并的类型项翻译为组合子仓库。
Stavi 定理的一个证明
简化证明 Stavi 定理：Until、Since 与 Stavi 模态的时序逻辑在所有线性序上表达力等价于 FOMLO。
加权 ω-受限单计数器自动机
将加权 ω-受限单计数器自动机的行为刻画为混合代数系统解的分量，并在 B 或 N∞ 下给出混合上下文无关文法生成构造。
类型 (ι → ι)^n → ι 的顺序泛函对所有 n ∈ N 构成 dcpo
证明了类型 (ι→ι)^n→ι 的顺序泛函构成 dcpo，并完整刻画了哪些类型具有该性质。
正则语言的差分层级综述
综述正则语言的差分层级，介绍Hausdorff经典技术，并给出shuffle理想、强循环正则语言与群语言多项式闭包的可判定性结果。
用于名字生成的证明相关逻辑关系
提出证明相关逻辑关系，为含递归的名字生成语言给出直接风格语义模型，并解决动态分配单子失效问题。
关于带二元关系的一阶谱的注记
证明多变量二元关系一阶句子的谱可线性归约到单一对称二元关系，且模型均为二部图，从而简化 Asser 猜想。
线性序上点与区间的集成一阶理论（第一部分）
对点-区间二排序一阶时序语言的子语言按相对表达能力进行完整分类，澄清点是否应纳入区间语义。
λμρθ-演算归约序列长度的估计
给出了带 ρ 和 θ 规则的 λμ-演算归约序列长度的上界，表明新增项与规则不增加计算复杂度。
具有可判定一元二阶理论的无限字与双向无限字
研究无限与双向无限字结构的可判定一元二阶理论，给出递归ω-字的复杂度刻画并比较二者异同。
Ologisms
提出 ologisms，将 olog 的等式约束扩展为可表达三段论约束，并借助图示逻辑演算实现。
全切换（all-switches）策略改进的复杂度
证明全切换策略改进中边是否被切换与最优策略问题均为 PSPACE 完全，覆盖多类图博弈。
用两个量词交替分离正则语言
证明有限基下任意串联层级 3/2 层的分离问题可判定，并将 dot-depth 推进到 5/2，从而解决 Σ3 的分离问题。
函数扩展中三个莱布尼茨原则的拓扑解释
在函数扩展框架下将莱布尼茨三原则分别解释为分离性、紧致性与有向性，并证明三者不能同时成立。
2017123 篇 · vol.Volume 13, Issue 2
从概率函数式程序推导概率密度函数
提出一种概率函数式语言的密度编译器，并为含失败及离散/连续分布的程序证明其可靠性。
匹配逻辑
提出匹配逻辑，一种以模式与模式匹配统一刻画结构和推理的一阶逻辑变体，可泛化多种程序分析逻辑并支持 SMT 求解。
单态与多态类型的编码
系统研究并实现将单态与多态类型编码到无类型一阶逻辑的方案，提升自动定理证明效率且保持可靠完备。
状态-效应三角（state-and-effect triangles）的构造配方
利用 Beck 单子性定理，从伴随系统化构造状态-效应三角，统一多种程序语义单子。
在类型论中实现类型论的正规化求值
在类型论内部用商归纳类型构造依赖类型的正规化求值，并证明定义相等可判定。
基于概率进程演算的组合性双模拟度量推理
提出用一致连续性刻画概率进程演算中双模拟度量语义的组合推理，并支持递归过程与度量式假设保证性能验证。
双模拟与抽象的博弈
用 Spoiler-Duplicator 博弈统一刻画分支、延迟、η 与弱双模拟，并辅助诊断实现与规约的不一致。
Innermost 重写的可达性分析
将树自动机补全算法扩展到 innermost 重写策略，以精确近似可达项集合，并在 Timbuk 中实现验证。
利用天使与恶魔非确定性的 Hoare 逻辑合成策略
提出一种命题 Hoare 逻辑，统一刻画天使/恶魔非确定性，支持部分正确性验证与策略合成，并证明其判定复杂度为 EXPTIME。
离散概率分布的 Hyper 正规化与条件化
将概率正规化从偏函数重构为输出分布之分布的全函数，并用于条件化与定量信息流 refinement。
LLF_𝒫：一个使用 monad 建模外部证据、边条件与证明无关性的逻辑框架
扩展 LF 提出 Lax Logical Framework LLF_𝒫，用 Lock monad 表达边条件、外部证据与证明无关性，并证明其保守性。
互模拟距离的即时计算
提出连续时间马尔可夫链互模拟距离的多项式线性规划刻画与高效即时算法，避免穷举状态空间。
时间化会话类型
提出时间化会话类型，给出判定合规性与构造最精确合规对端（及子类型可判定性）的可靠完备技术。
非确定性与概率 Büchi 自动机的公平模拟：一个余代数视角
从余代数视角统一推广 Büchi 自动机的公平模拟至非确定树自动机与概率字自动机，并证明其可靠性。
过程间双变量 Herbrand 等式
提出过程间推断所有有效双变量 Herbrand 等式的分析方法，并给出多项式时间不变式验证。
一种面向数据库的协调语言
提出数据库协调语言 Klaim-DB，给出其形式语义与类型系统，以排除求值错误和表数据格式不匹配等运行时错误。
Parity 与 Streett 目标的改进算法
提出求解 parity 和 Streett 目标获胜集的新算法，15 年来首次改进渐近时间复杂度。
面向闭包空间的空间逻辑模型检测
提出基于闭包空间的空间逻辑，并给出个体与集体片段的模型检测算法及原型工具。
Martin-Löf 类型论中的匿名存在概念
刻画具有唯一恒等证明的类型，基于弱常值自函数与命题截断提出匿名存在概念，并在 Agda 中验证。
用于服务契约规约与编排的自动机
用自动机形式化描述服务契约，并在同步/异步多主体组合中构造编排器以保证请求满足。
基于遗忘逻辑的余代数迹语义
提出用遗忘模态逻辑统一刻画余代数迹语义，并给出其与确定化构造一致及典范确定化存在的条件。
基于不动点的计算场的异步分布式执行
提出 SMuC 演算及分布式实现，证明公平异步与节点重初始化下不动点计算收敛。
通过类型系统保证诚实性
提出面向契约进程演算的类型系统，保证可类型化进程在所有上下文中诚实，并给出可判定的类型推断。
QBF 归结演算的可行插值
为所有基于归结的 QBF 证明系统建立可行插值技术，并给出首个通用指数下界方法。
类型论中马尔可夫原理的独立性
证明马尔可夫原理在含自然数和一个宇宙的依赖类型论中不可派生，并给出保持一致性的扩展及规范化论证。
通过近似反向翻译实现模块化的完全抽象编译
提出只需构造近似反向翻译的通用技术，使源语言无法嵌入目标语言时仍能证明编译器完全抽象。
追踪 IoT 数据的收集与聚合位置
提出 IoT-LySa 进程演算及静态分析，追踪 IoT 数据来源、聚合与流动，以支持安全等非功能性质验证。
行为良好的迁移系统
证明仅需无无限反链的单调迁移系统仍可判定覆盖性，并定义其严格超类 WBTS。
精细化传值 λ-演算的标准化与保守性
通过两条交换规则扩展 Plotkin 传值 λ-演算，证明其是保守精细化并建立弱标准化定理。
统一马尔可夫决策过程中多均值收益目标的两种视角
统一 MDP 中多均值收益目标的期望语义与满足语义，并给出多项式时间算法与策略复杂度刻画。
一个面向经验证自稳定性的框架
在 Coq 中建立自稳定算法的通用认证框架，并验证 k-聚类算法的部分正确性与簇头数量上界。
幺半范畴的相干表示
推广范畴的生成元-关系表示，证明在对象模等价时商、局部化与正规形三种构造在相干条件下一致，并扩展至幺半范畴。
自由局部笛卡尔闭范畴中等式的不可判定性（扩展版）
证明外延 Martin-Löf 类型论构成自由 CwF，并归约证明自由局部笛卡尔闭范畴中等式不可判定。
论布尔逻辑的线性重写系统及其在证明论中的一些应用
证明布尔逻辑中仅含线性推理的重写系统其非平凡推导长度多项式有界，并推出不存在多项式时间可判定的完备线性推理系统，除非 coNP=NP。
数据字上 MTL 与 TPTL 的路径检查
精确刻画 MTL 与 TPTL 在非负整数数据字上的路径检查复杂度，并导出确定性单计数器机模型检测的复杂度。
论定量信息流的组合性
提出用各组件泄漏量界定整体系统 g-leakage 的组合性边界，并推广 min-entropy 泄漏与并行信道结果。
下推自动机的编辑距离
完整刻画了下推自动机到有限自动机编辑距离的阈值判定与有限性判定的可判定性和复杂度。
具有动态提示生成的多提示定界控制算子的环境互模拟
为支持动态提示生成的多提示定界控制演算提出可靠且完备的环境互模拟，并给出新的 up-to 证明技术。
π演算中基于类型的隐私
提出带组的π演算扩展Pcalc及类型系统，通过类型与隐私策略的可满足性确保系统遵守策略。
弱 MSOL 性质的类型化
为 λY 演算设计类型系统，确保程序正规形满足给定的弱一元二阶逻辑性质。
内涵类型论中的幂等元
研究内涵类型论中幂等元的分裂问题，给出可分裂的相干条件并构造不可分裂反例。
易于取胜，难于精通：带成本的奇偶博弈中的最优策略
本文证明带成本奇偶博弈中求最小成本界的最优策略问题 PSPACE 完全，且指数记忆必要且充分。
多参与方会话 Actor
将多参与方会话类型引入 Actor 模型，通过角色与协议邮箱在 Python 中实现运行时通信安全验证。
判定迹等价的约简语义
提出约简符号语义与偏序归约，消除冗余交错，加速安全协议的迹等价判定。
论 Herbrand 构造逻辑的自然演绎 I：Dummett 逻辑 LC 的 Curry-Howard 对应
为 Dummett 逻辑 LC 建立一阶与二阶自然演绎及 Curry-Howard 对应，并证明其类型化演算可规范化并导出 Herbrand 析取。
迈向级联效应的代数
提出一类可组合的动态系统及其公理化代数，用格与不动点刻画级联效应、失效、韧性与脆弱性。
守卫 λ-演算：面向余归纳类型的守卫递归编程与推理
提出带守卫递归与余归纳类型的 λ-演算，保证良类型程序的生产力，并给出指称语义与程序逻辑。
将 EL 中的合一扩展到去合一：dismatching 与局部去合一的情形
研究 EL 描述逻辑中带负约束的去合一问题，证明 dismatching 与局部可解性为 NP 完全。
通过变换和矩阵解释证明循环重写的终止性
提出三种可靠完备变换及统一矩阵解释框架，证明循环重写及其相对终止性。
构建你自己的 clarithmetic I：系统设定与完备性
提出参数化理论 CLA11，通过调参得到相对于三复杂度类的可靠且完备算术系统，并证明完备性。
发现、量化并展示攻击
提出基于 Quality Calculus 的保护分析，可发现攻击、按代价量化最廉价攻击并生成攻击树。
无限字语言中的有界性
定义扩展 ω-正则语言的无限字语言类，用有界/无界 Kleene 指数与自动机刻画，并给出可判定与封闭性结果。
源自无类型 λ 演算稳定模型的一个经典可实现性模型
从相干空间的无类型 λ 演算稳定模型构造经典可实现性模型，并用 bar recursion/induction 验证可数选择。
通过相对终止与规则标记认证合流性证明
在 Isabelle 中形式化相对终止与规则标记结合的合流性判定准则，并集成到 CeTA 以检查基于递减图的合流证书。
若干开集格的一阶理论
证明若干自然拓扑空间的开集格一阶理论与二阶算术 m-等价，并刻画有效开集格理论的可判定性。
形式语言：形式化与余归纳
在 Isabelle 中以无限 trie 的余归纳表示形式语言，定义正则运算并证明 Kleene 代数公理，证明自动化优于词集合视角。
Statman 层级定理
以自足构造性方式重证简单类型λ演算中类型可归约层级定理：≤_{βη} 的序型为 ω+4，并细化出 ω+5 与 8 的层级。
块结构 vs 作用域外逸：介于 innocence 与 omniscience 之间
用博弈语义中的 block-innocent 策略刻画块结构，并比较块存储、纯函数式计算与动态内存分配。
会话契约的可撤销性、博弈与编排器
扩展会话契约以支持可受第三方或双方协议影响的输出，并用三方博弈与编排器刻画其合规性。
基于二阶代数理论的模双模拟循环数据类型
提出基于二阶代数理论的循环数据类型框架，提取 fold 规则并证明强正规化、Church-Rosser 模双模拟及等式可判定性。
可编程策略到项重写系统的忠实（元）编码
将可编程策略忠实编码为项重写系统，使策略控制重写的终止性可用现成终止工具分析。
序列决策问题、依赖类型与通用解
用依赖类型语言给出有限时程序列决策问题的计算机检查通用实现与贝尔曼最优性原理证明。
约束自动机的数据优化
为约束自动机编译器提出并证明两项数据约束处理优化，提升生成代码性能。
为带计数的守卫二变量片段添加路径函数依赖
证明加入路径函数依赖与数据库后，带计数量词的守卫二变量片段的可满足性与有限可满足性均为 ExpTime 完全。
在存在 alldifferent 约束时求解有限域线性约束
提出一种利用 alldifferent 约束信息来强化有限域线性约束过滤与变量界的改进算法。
乘法-加法证明等价性是 Logspace 完全的，经由二叉决策树
线性逻辑乘法-加法片段的证明等价问题经二叉决策树归约，精确复杂度为 Logspace 完全。
动态编排：理论与实现
提出动态编排语言AIOC并编译为APOC，保证运行时更新后分布式应用仍无死锁与竞态。
关于策略的推理：可满足性问题
提出单目标策略逻辑 SL[1G]，证明其具有有界树模型性质且可满足性是 2ExpTime 可判定的。
作为事件结构的博弈与策略
以事件结构统一刻画并发博弈与策略，构造双范畴并证明其紧致闭结构，为并发高阶计算提供语义基础。
概率与非确定性的混合幂域
为概率与非确定性混合选择建立三类幂域，给出自由代数、函数表示及状态/谓词转换器等价。
论会话类型中子类型的精确性
证明同步会话演算中分支-选择子类型既可靠又完备，并构造异步演算下可靠完备的子类型系统。
Lineal：一种线性代数 Lambda 演算
提出扩展 Lambda 演算的线性代数演算 Lineal，允许任意线性组合项，给出重写规则并证明合流。
赢得无限博弈需要多少前瞻量？
将 ω-正则延迟博弈的求解复杂度与所需前瞻量从双指数改进为指数，并给出紧界。
数据树上的自底向上自动机与垂直 XPath
提出一种数据树自底向上交替自动机，证明其刻画垂直 XPath，并给出可满足性判定。
Cook 理论 PV 中电路上界的不可证明性
无条件证明每个 k 都存在 P 语言 L，使 PV 不能证明 L 不属于 Size(n^k)。
描述逻辑本体的数据复杂度
研究单个描述逻辑本体在合取查询等查询下的数据复杂度，给出 PTime/coNP 二分与不可判定性结果。
关于形式球的若干注记
借助形式球偏序集上的域论构造，统一给出拟度量空间的一系列新结果。
论一阶直觉主义逻辑中的 Mints 层级
证明一阶直觉主义逻辑 Mints 层级中 Δ2 不可判定、Σ1 为 Expspace-完全，并刻画元数受限 Σ1 的复杂度。
流微分方程：规格格式与求解方法
综述流微分方程的多种规格格式、求解方法及其可定义流类，并阐明语法解法与抽象 GSOS 的联系。
多重树自动机的最小化
给出有理数域上多重树自动机状态数最小化的多项式时间算法，并将其复杂度与多项式恒等测试相联系。
不相交并偏代数
为集合与偏函数上的不相交并等偏代数给出递归一阶公理化，证明其不可有穷公理化，并考察加入交集后的可公理化性。
Petri 自动机
提出 Petri 自动机识别有向标号图，证明对应 Kleene 定理，并确定无单位关系 Kleene 格等式理论为 EXPSPACE-完全。
条件项重写的复杂度
为带限制的定向条件项重写系统提出更现实的复杂度概念，并归约到无条件上下文敏感重写系统以推导复杂度界。
代数代数的若干方面
研究 Kock-Zöberlein 单子的中间范畴，刻画自由代数与加权（余）极限，并给出 filter 单子 Kleisli 范畴的幂等分裂完备化。
多主动对象及其应用
提出多主动对象编程模型，用 ProActive 库和 MultiASP 语言形式化，并给出协作式多线程主动对象到多主动对象的编译。
可计算拓扑中的 Rice-Shapiro 定理
给出有效可枚举拓扑空间上 Rice-Shapiro 定理成立的条件，并构造反例刻画其失效边界。
关于 Quantale 值拓扑空间的拓扑性的注记
在 V 为空间余框架的较弱条件下，无选择公理地证明 V-拓扑空间范畴是 Set 上的拓扑范畴。
Goursat 范畴中连接子与群胚的若干注记
证明了 Goursat 范畴中连接子在商下稳定，并由此给出内群胚刻画 Goursat 范畴的简洁性质。
计算若干线性双曲偏微分方程系统边值问题的解算子
用数值分析与TTE框架证明对称双曲PDE系统边值问题解算子的可计算性。
构建你自己的 clarithmetic II：可靠性
为参数化 clarithmetic 系统 CLA11(P1,P2,P3,P4) 证明可靠性，并说明其定理对应可提取的复杂度受限算法解。
论会话与无限数据
提出结合按名调用函数核心与会话通信的演算，类型系统保证表达式规范化与进程推进。
广义树的代数与逻辑描述
用有限代数运算与无穷项生成拟树、联接树，并证明其正则对象恰为 MSO 句子的唯一模型。
余代数模态 μ-演算的表达完备性定理
提出余代数上的一元二阶逻辑，并给出余代数模态 μ-演算恰为其行为不变片段的充分条件。
通用进程
在进程演算中形式定义通用进程，并构造值传递演算的通用进程，进而嵌入递归论。
通过可及像的 Hanf 数
在大基数假设下用可及函子的可及像，将 AEC 的 Hanf 数结果推广到可及范畴，并证明度量 AEC 强 d-tame。
复杂度层级与高阶 cons-free 项重写
论文证明左线性 cons-free 高阶项重写系统按类型阶 K 刻画 E^K TIME，并分析非确定性与语法限制的影响。
代数交集类型合一问题
证明代数交集类型合一问题是指数时间困难的，并给出 rank 1 解与匹配问题的不可处理性下界。
有界度谱与平面谱
刻画平面与有界度限制下一阶有限谱的表达力：包含 NE 的重要片段，但并非全部 NE 集合。
π 演算的内涵全抽象层模型（扩展版）
为 π 演算构建层语义模型，并证明其对公平测试等价是内涵全抽象的。
均匀化问题的 Borel 分段连续可归约性
研究 Borel 分段连续函数的细粒度层级，并据此分离集合值函数均匀化问题及 Weihrauch 格中的非构造性原则。
正交逻辑中的聚焦
为正交逻辑提出满足切消的新序演算系统，并引入线性逻辑的聚焦以优化自动证明搜索。
一致空间的 localic 完备化
把 Vickers 的 localic 完备化从广义度量空间推广到广义一致空间，并证明其与 Cauchy 滤子完备化一致。
由偏序禁止模式定义的 CSP 中弧相容性的力量
刻画了偏序禁止模式定义的二元 CSP 中弧相容可解的五个模式，扩展 BTP 并发现新易解类。
论带模计数量词的 arb-invariant 一阶公式的局部性
刻画 arb-invariant FO+MOD_p 的 Gaifman 与 Hanf 局部性，并给出正负结果及其与布尔电路的联系。
对偶化简单类型理论
提出带完美直觉主义对偶性的简单类型论 DTT，对应单侧极化序列演算，并证明强规范化与类型保持。
论 S-原模范畴中的若干范畴代数条件
为 S-原模范畴引入相对化附加条件，建立其类群行为的层级。
单子-Quantale-富化范畴中的松弛正交因子分解
证明 (T,V)-范畴上的预层单子是 simple 的，由此构造松弛正交因子分解系统，其弱系统左部为 embeddings。
构造性分析中的 Z-稳定性
引入 Z-稳定性概念，研究其点态与一致版本，并给出构造性过渡所需条件与递归反例。
基于可实现性语义的简单类型 λμ-演算的修正完备性结果
为简单类型 λμ-演算提出新的可实现性语义，并用项模型证明其完备性，修正了此前工作中的错误。
Dickson 引理的一个界
为 Dickson 引理的一个特例构造显式界，并通过 realizability 从形式化证明中抽取该界。
作为有理幺半群的规范 BPA 过程分支互模拟等价
将规范 BPA 过程的分支互模拟等价刻画为有理幺半群，并给出由正规形确定有限转换器判定的分解框架。
随机归结的可行插值
将语义推导的可行插值定理应用于随机归结，并由此得到团-着色公式随机归结反驳的下界。
关于函数性质从局部到整体存在的一些定理
提出强联合允许性概念，并给出递归函数、连续函数及有效拓扑可计算情形下局部性质扩展到并集的充要/充分条件。
非标准分析中的 Grilliot 技巧
利用非标准分析中的标准外延性技巧，从非标准不连续泛函导出图灵跳跃泛函的有效蕴含。
逻辑紧致性与约束满足问题
揭示约束满足问题复杂度层级与有限关系结构上的逻辑紧致性假设层级之间的对应关系。
强 proper dyadic 子基的存在性
证明每个局部紧可分离度量空间都存在强 proper dyadic 子基，从而获得可容许的 domain 表示。
条件可计算实函数的刻画定理
在不使用无穷名称的情况下，给出条件可计算实函数的表征定理。
λ-Sym-Prop 与 λ̄μμ̃* 演算的强归一化
以算术方法证明 λ-Sym-Prop 强归一化，并用 zoom-in redex 序列给出其与 λ̄μμ̃* 的翻译。
可积函数空间的复杂度理论
为可积函数与 Lp/Sobolev 空间建立二阶表示，刻画积分、微分等运算的多项式时间可计算性与表示最小性。
从逻辑经物理到生物学：一项综述
综述从逻辑与物理视角理解生物有机体，强调不完备性、随机性和理论对称性在生物动力学中的作用。
完备 Heyting 与 co-Heyting 代数的新刻画
为完备 Heyting 与 co-Heyting 代数给出新的序理论刻画，并揭示其与 Nash 均衡的意外联系。
次可计算 Schnorr 随机性
为次可计算类提出 Schnorr 随机性概念，并用 Martin-Löf 检验、鞅与测度可计算机器加以刻画。
半加性簇中的 Hopf 与 Lie 代数
在熵半加性簇中研究 Hopf 幺半群，并刻画包络幺半群函子与原始元素函子之间的伴随关系。