LICS（CCF A）（共 679 篇）
2025 起转 LIPIcs（开放获取），DBLP conf/lics stream 覆盖全部年份
202566 篇 · 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
随机变量、条件独立与抽象样本空间范畴
从合适 Markov 范畴构造满足 Simpson 公理的样本空间范畴，并合成式建立概率层理论。
并发随机可达性与安全性博弈中值迭代的停止准则
为并发随机博弈的值迭代提出带上/下界的停止准则，保证近似精度。
等价超图：幺半群 E-Graph 的 DPO 重写
为幺半群 e-graph 建立范畴语义与 e-超图表示，并实现 DPO 重写。
最小历史确定性 co-Büchi 自动机：同余与被动学习
用同余刻画最小历史确定性 co-Büchi 自动机，并给出多项式时间被动学习算法。
马尔可夫模型中的乘性奖励
研究马尔可夫链与MDP中乘性奖励期望值/最优值的计算问题，给出复杂度刻画与算法。
如果起初不成功：通过多次执行扩展可监控性
研究利用多次系统运行监控分支时间性质，证明可系统扩展传统可监控性边界并给出运行次数界。
笛卡尔微分范畴中的组合式泰勒展开
在笛卡尔微分范畴中用函子与单子刻画泰勒展开，统一高阶导数、对偶数与 jet bundle。
可达性条件下的初始代数对应
提出统一范畴框架，用伴随刻画可达性条件，使转移系统的两种不动点/初始代数语义一致，并实例化到马尔可夫链与自动机。
高阶逻辑中的句法效应化可实现性
提出 EffHOL，将句法可实现性推广到带副作用的计算，并通过 monad 参数化抽取效应化实者。
线性动力系统中的多重可达性
证明线性动力系统多重可达性在 d=10、m=9 时不可判定，并给出二维平面中旋转矩阵与半平面目标的可判定性。
算子空间、线性逻辑与量子理论的 Heisenberg-Schrödinger 对偶
证明算子空间范畴可建模直觉主义与经典线性逻辑，并使其对偶与量子理论的海森堡-薛定谔对偶相容。
带名称分配的交替名义自动机
引入正则交替名义自动机，证明无界寄存器下非空与包含仍为初等复杂度，并几乎完全去交替化。
在数环上学习加权自动机：具体与范畴论方法
提出主动学习通用归约，并给出数环上加权自动机的多项式时间精确学习算法，输出近最小自动机。
多项式时间内学习确定性单计数器自动机
提出黑盒主动学习算法 OL*，在多项式时间内学习确定性单计数器自动机，并可用于近似最小化。
补全 Gordon 的高阶逻辑
为 Gordon 的 HOL 引入 Henkin 式一般模型，并证明一种增强演绎系统相对这些模型既可靠又完备。
同伦类型论中的序数指数运算
在同伦类型论中给出构造性序数指数的两种定义，证明其等价并形式化验证代数律与可判定性。
基于 lax 耦合的行为一致性
提出松弛耦合构造，为余代数系统定义行为距离与前序，扩展其可表达范围。
带效应的 Mealy 机：互模拟与迹
提出带全局效应的 Mealy 机，以自由一致反馈刻画互模拟，并用带效应流建立迹的余代数语义。
基于累积前景理论的风险感知马尔可夫决策过程
为MC和MDP的累积前景理论值建立多目标可达性联系，给出策略复杂度与EXPTIME算法。
有效形式级数簇的交换性问题及其应用
证明对构成有效预簇的形式级数类，交换性可判定，并应用于多项式/洗牌/渗透自动机与代数差分方程。
时序因果性的闭包性质与复杂性
证明安全、可达与重现性质的因果推断具有闭包性，并给出计算原因的更优上界及所有性质类的下界。
经由无序 join 的 Steenrod 平方
在同伦类型论中通过无序 join 这一高阶归纳类型证明 Steenrod 平方的核心性质，并给出 Cubical Agda 形式化。
正则整数线性指数规划的量词消去
用量词消去判定正则整数线性指数规划，保持 ExpSpace 上界，并证明特定正则整数线性规划 PSPACE 完全。
翻转与分叉
在任意关系结构上引入翻转与翻转独立，证明其与模型上的分叉独立等价，统一单子稳定类的组合刻画。
同步块图编译器的函数式流语义
为同步块图编译器给出函数式流语义，并重述其端到端正确性定理。
模糊的饮酒者悖论：向下 Löwenheim-Skolem 定理的构造性反推数学
在构造性反推数学中精细分解向下Löwenheim-Skolem定理，提出模糊饮酒者悖论BDP并刻画其与选择公理的关系。
单值范畴的内部语言
将内部语言定理推广到单值范畴与多种拓扑斯，并用 Rocq/UniMath 形式化。
论带不动点的线性逻辑中循环与非良基证明的指称语义
为带最小/最大不动点的线性逻辑 μLL 的非良基与循环证明建立范畴语义，并证明翻译保持解释。
二变量逻辑的模型枚举：二次延迟复杂度
提出 FO2 模型枚举算法，在固定句子下延迟复杂度为 O(n² polylog n)，接近理论下界。
带嵌套零测试的向量加法系统中的可达性及相关问题
证明带嵌套零测试的 VASS 可达性具有 Ackermann 上界，并统一判定半线性、可分性等相关问题
单计数器自动机中半线性目标集的复杂度二分
为单计数器整数 VASS、Parikh 自动机与标准 VASS 的广义可达性问题建立三条 AC1/NP 完全复杂度二分定理。
偏映射分类器何时是 Sierpiński 锥？
在单值基础中研究偏映射分类器与 Sierpiński 锥的关系，证明合成 ∞-范畴在 Phoa 原则下对其封闭，并刻画可计算该锥的反射子宇宙。
基于最优传输对偶的完备量子关系霍尔逻辑
提出基于最优传输对偶的完备定量量子关系霍尔逻辑，并可嵌入投影断言逻辑。
单纯类型论中的 Yoneda 嵌入
在单纯类型论中构造预层范畴与 Yoneda 嵌入，并发展 ∞-范畴论工具。
双向模态 μ-演算的插值性质
为双向模态 μ-演算引入非良基与循环矢列证明系统，证明其可靠完备，并推出 Craig 插值与 Beth 可定义性。
可达性类型、迹与完全抽象
首次为可达性类型建立可靠迹模型并精化为完全抽象语义，并给出情境近似结果。
下推模型检测：超越三次瓶颈
证明下推模型检测的 O(n^{2k}|Σ|+n^{3k}) 上界在 3k-clique 假设下已接近最优。
概率策略：可定义性与张量完备性问题
论文研究 I/O 与可数概率选择程序形成的概率策略，用等式理论的和与张量刻画双相似和迹等价，并在有穷情形证明完备性。
CK 与 IK 之间直觉主义模态逻辑的语义分析
为 CK 与 IK 之间的直觉主义模态逻辑给出 Kripke 语义与框架条件，解答其相对无 diamond 逻辑的保守性问题。
3D-grid 无法从平面图转导得到
证明 3D-grid 类不能从平面图及任何有界亏格图类转导得到，并提出切片分解这一新结构工具。
正则语言的导航层级
引入基于一元时序逻辑算子的导航层级来分层星自由语言，并证明其与拼接层级的关系及若干可判定性结果。
高维路径类型的自然性
在依赖类型论中为弱 ω-范畴操作定义自然性构造，用于生成并验证高维路径项。
高阶等式理论的同调不变量
将同调方法推广到高阶等式理论，用同调群计算等式公理数量的下界。
一阶逻辑带平均算子扩展的收敛律
证明若干一阶逻辑收敛律可扩展到带平均聚合算子与Lipschitz连接词的实值逻辑。
Call-by-push-value 模型的逻辑关系：经由 2-范畴中的内部纤维化
用 2-范畴内部纤维化为 CBPV 建立逻辑关系语义框架，并给出 ⊤⊤-lifting、效应模拟与相对完全性等实例。
带计数的二变量一阶逻辑片段中的分离与可定义性
研究带计数量词的二变量一阶逻辑及分级模态逻辑中可定义与分离问题的可判定性和复杂度。
Promise 与无限域 CSP 之间的代数与算法协同
建立框架在 promise CSP 与无限域 CSP 间转移结果，给出新的 NP 难判定及时间约束多项式算法。
再探 Relator 与模拟概念
在余代数框架下系统研究 relator，揭示其与（双）模拟闭包性质、可靠完备性及松弛扩张的对应关系。
代数数上几乎可解矩阵群中的恒等问题
证明代数数上几乎可解矩阵群的恒等问题与群问题可判定，显著缩小已知不可判定边界。
并发博弈的定性坍缩
构造从并发博弈到 Scott 域的保解释函子，给出定性模型提取定量信息的组合描述，并重证 Ehrhard 定性-定量对应。
光滑有向图的忧伤：无限有向图着色问题的首个硬度判据
首次将代数长度为 1 的光滑有向图结构二分类提升到无限域，给出无限有向图着色的 NP 难判据。
纤维范畴的 Hofmann–Streicher 提升：纪念 Thomas Streicher (1958–2025)
基于 Awodey 的范畴神经分析，给出 Hofmann–Streicher 宇宙提升的纤维范畴相对版本。
具有无界线性团宽的图必然可转导所有树
证明图类若线性团宽无界，则存在固定 MSO 转导可由其生成所有树，将路径宽度定理推广到稠密图。
分级语义的符合性博弈
将分级语义的通用行为等价博弈推广到行为符合性，统一刻画前序、伪度量等进程比较并给出可靠完备博弈。
量子 CSP 策略的经典模拟
证明两证明者 CSP 博弈的完美量子策略可由带额外经典通信的完美经典策略模拟，通信量受量子系统与 CSP 模板约束。
薄余代数行为是归纳的
证明薄余代数可由初始代数归纳刻画，并给出其语法与单方程公理化。
#P 被一次与两次 #2DNF 调用夹在中间：减法比我们想象的更强吗？
证明两次（或一次加后处理）#2DNF 调用的减法即可刻画 gapP，从而把 #P 严格夹在一次与两次调用之间。
定量二阶查询的近似求值
推广 Courcelle 定理，提出 \boxed\forall CMSO 逻辑，为树宽/团宽参数化问题提供 1/ε 多项式时间近似方案。
群阶逻辑
提出带群阶算子的不动点逻辑 FP+ord，可多项式时间模型检测，并刻画更广的多项式时间可计算查询。
基于次原子逻辑与守卫替换的证明压缩
提出守卫替换机制，在次原子逻辑中压缩证明，并可无需 cut 多项式模拟带替换的 Frege 系统。
FC-可定义正则语言的刻画与可判定性
证明存在非 FC-可定义的正则语言，并给出 FC-可定义正则语言的可判定刻画与表达式形式。
树宽至多为 2 的图集合的正则文法
将正则文法从词推广到无序无秩树与树宽至多 2 的图，并刻画其可识别/CMSO 可定义集合及复杂度。
带变量绑定与单变量替换的子结构抽象语法
为线性、仿射、相关和笛卡尔子结构下的带变量绑定抽象语法建立统一的范畴论，并刻画单变量替换。
容许乘积结构的图类的一阶转导
证明乘积结构图类的一阶转导可由 H-clique-width 刻画，并据此分离 3D 网格与平面图。
可处理非刚性结构的二元对称性
分类任意置换群上的最小操作，并证明缺少二元本质 polymorphism 可致非刚性结构 CSP NP-hard。
有界路径宽的有限域可表示拟阵：可识别性等于可定义性
证明有界路径宽的有限域可表示拟阵上，可识别性等价于 MSO 可定义性。
202472 篇 · Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science
无元素概率分布与随机划分
用多重集和范畴论建立无元素概率分布理论，并给出交换随机划分与随机分布的表示定理。
下推正规形式互模拟：一种面向程序等价的名义上下文无关方法
提出下推正规形式互模拟，可可靠、完备且对调用栈无界情形可判定地验证高阶函数式程序上下文等价。
概率分离逻辑的 nominal 方法
证明概率论中的概率空间乘积分解与概率分离逻辑中的测度论分解在范畴等价意义下等价。
原子层逻辑（Atomic Sheaf Logic）中的等价与条件独立
提出原子层拓扑语义框架，统一解释变量等价与条件独立，并在经典逻辑中验证基本推理原则。
随机变量的笛卡尔闭范畴
在 Scott 域框架下构造随机变量域，建立概率编程语义的笛卡尔闭范畴与四个强交换单子。
论插值算法的完备性
首次系统研究插值算法的完备性，证明若干归结与相继式演算标准插值算法的不完备性及多种完备性。
仿射连续 VASS 判定问题的可判定性与复杂度
本文对仿射连续 VASS 的可达、覆盖与状态可达问题给出近乎完全的可判定性分类与紧复杂度界。
线性终止是不可判定的
通过从希尔伯特第十问题归约，证明单规则重写系统线性解释终止性不可判定，并扩展至多种序与多项式解释。
结合不动点理论与微分理论
提出带不动点算子的笛卡尔微分范畴，并用新公理刻画微分与不动点的交互，应用于 Newton-Raphson 优化。
通过嵌套数据的状态与控制情境等价
证明有限无递归的 ML 风格语言中一阶引用与续延程序的情境等价可判定，并归约为嵌套数据自动机等价。
重置工作流网的健全性
证明重置工作流网的广义健全性不可判定，并提出介于1-健全性与广义健全性之间的可判定性质“1-in-between健全性”。
局部一致性作为约束满足问题之间的归约
提出一致性归约框架，用局部一致性刻画 promise CSP 的归约与硬度，并联系多态性与 Sherali-Adams 层级。
量子电路的极小等式理论
首次给出量子电路的极小且完备的等式理论，并证明任何完备等式理论都需作用于无界数量量子比特的规则。
混合选择多参与方会话中的分离性与可编码性
提出混合选择多参与方会话类型系统并证明可靠性，用可编码与分离性比较九个子演算的表达力。
一阶逻辑的图解代数
提出新皮尔士关系演算，用弦图给出一阶逻辑表达力的二元关系演算及其完备公理化。
量子超映射的 profunctor 语义
用强 profunctor 的态射将量子超映射范畴化，并给出理论无关的抽象逻辑连接词与分解定理。
准稠密模态逻辑的可判定性
证明准稠密模态逻辑可判定，并给出基于模板枚举的 ExpSpace 判定过程。
VASS 可达语言的可分离性问题
证明 VASS 可达语言的正则可分离性可判定且为 Fω-完全，并引入双标记图转移序列分解算法。
Mazurkiewicz 迹上表达完备的局部过去命题动态逻辑及其应用
提出 Mazurkiewicz 迹上局部过去命题动态逻辑，证明其相对正则迹语言表达完备，并构造异步自动机级联积。
高阶程序等价性的双代数推理
提出高阶数学操作语义下逻辑关系的通用构造，并证明其对上下文等价自动可靠。
通过 Amalgamation 验证无界性
提出运行集带良拟序且支持融合的抽象系统，统一 VAS、PDS 等，并给出无界性问题的通用判定算法。
通过分层归约实现泛性
用分层归约证明 CbV 中可审查性刻画有意义项，并给出泛性与一致性结果。
基于此 quote，我将建立我的丘奇论题
通过带 quote 算子的 MLTT 扩展，正面证明内部丘奇论题与依赖类型理论兼容，并建立其元理论。
组合 Codensity 双模拟
提出在代数与余代数层面使用 codensity 提升，给出分配律可提升的充分条件，统一证明各类状态系统上行为等价的组合性。
相关逻辑 S 是不可判定的
证明半格相关逻辑 S 的判定问题不可判定，推翻其可判定猜想。
概率正则表达式的完备性定理
引入概率正则表达式，并证明其基于Kleene代数公理化的概率语言等价推理系统具有完备性。
稀疏图的一阶模型检测：初等复杂度刻画
几乎完整刻画了子图封闭图类上一阶模型检测何时以初等依赖于公式大小的固定参数算法可解，并证明排除固定树作为拓扑子式即可。
带实值折扣因子的折扣和自动机
证明当折扣因子为 Pisot 数时，实值折扣和自动机保持整数情形的良好闭包与可判定性。
论带算术谓词的一元二阶逻辑的可判定性
研究带算术谓词的自然数序结构的一元二阶理论可判定性，并给出若干无条件与条件性判定结果。
No-Go 定理：不能分配到分布单子上的有向容器
证明有向容器等余单子不能对幂集/分布单子等统一选择单子形成分配律，给出一类 no-go 定理。
索引语言的切片闭包与带计数约束的词方程
证明可计算索引语言 Parikh 像的最小切片半线性表示，并据此判定词方程计数约束。
PCTL 的有限可满足性问题是不可判定的
证明 PCTL 的有限可满足性不可判定，甚至受限公式类和有限状态 Markov 链有效性也不可半判定。
关系机器演算
提出关系机器演算 RMC：一阶关系编程的基础模型，以语法对合与 Frobenius 幺半群字符串图统一多种计算模型。
从量词深度到量词数量：用 k 个变量区分结构
利用 QVT 博弈研究 k 变量一阶逻辑中区分两个结构所需的量词数，并证明其与量词深度可指数分离。
一元权重折扣和博弈的确定性次指数时间算法
为权重一元表示的折扣和博弈提出策略迭代的新分析，给出确定性次指数时间上界。
面向程序复杂度分析的脱密策略
提出一种保持 FP 可靠性的脱密策略，放宽非干扰类型系统以接受更多多项式时间程序，并刻画 BFF。
δ 代表 Dialectica
揭示反向传播与 Gödel Dialectica 解释的意外联系，并连接到微分 λ 演算与微分线性逻辑。
初始代数不再受链约束：一种在 Agda 中形式化的新初始代数构造
提出不依赖序数链、取所有有限递归余代数之余极限的初始代数构造，并在 Agda 中构造性形式化验证。
使用 epsilon-项在深度推理中实现一阶证明的非初等压缩
提出 falsifier 演算，用 falsifier 规则引入 epsilon 项，使某些一阶定理的无切证明可非初等压缩。
二变量一阶逻辑中正则关系的一致化
为 FO2[<] 定义的正则关系一致化问题给出判定算法，并提出该逻辑可定义语言的新表示。
位置性 ω-正则语言
通过刻画识别位置性语言的奇偶自动机，给出 ω-正则语言位置性的判定特征与封闭性结果。
在拓扑子式自由图类上模型检测不相交路径逻辑
证明在排除固定拓扑子式的图类上，带不相交路径谓词的一阶逻辑模型检测是固定参数可处理的。
1-in-3 与 Not-All-Equal：一个被打破的 promise 的二分性
研究 promise 被 rainbow-free 结构从任一侧削弱后的 1-in-3/Not-All-Equal CSP，并建立复杂度二分性。
多项式歧义有理加权自动机的确定化与无歧义化
证明多项式歧义有理加权自动机的确定化与无歧义化问题均在 PSPACE 中可判定。
双范畴中的效应语义：强、交换与并发伪单子
在双范畴中建立强/交换单子理论并提出并发伪单子，为并发函数式程序的效应语义提供统一框架。
分离 Markov 原理
澄清构造数学中三种 Markov 原理变体的强度关系，并证明它们严格分离。
多项式的等变理想
研究等变多项式理想的有限基，扩展 Buchberger 算法计算 Gröbner 基并判定成员问题。
带破坏的完备博弈逻辑
提出带破坏的博弈逻辑 GLs，证明其表达力等价于模态 μ-演算，并给出完备的 Hilbert 证明演算。
单值基础中的球面对称性
在单值基础中刻画球面自同构：圆的自同构为两个圆，高维球面自同构分两类且基本群为 Z/2Z。
通过值约束满足问题研究 resilience 问题的复杂度
将数据库 UCQ 的 resilience 问题归约为无限域 VCSP，给出硬度与多项式可解条件，并对无环情形得到复杂度二分。
量子优势与 CSP 复杂度
证明量子优势的出现由刻画 CSP 多态恒等式与复杂度的 minion 决定，并给出图与一般关系结构上的刻画。
部分信息博弈中的有界内存策略
研究部分信息多人随机博弈中有界内存策略的求解复杂度，给出近似零和值的NP难性与ε-Nash均衡的PSPACE、FNP^NP上界。
基于循环证明的右线性（ω-）文法证明论
提出右线性代数 RLA 与循环证明系统 CRLA，证明其对正则语言及 ω-正则语言的可靠完备性。
定量语义中的对称性分析
在 thin spans of groupoids 中分析定量语义的对称性，并将其与加权关系模型及 generalized species 的计数联系起来。
同伦类型论中用透镜空间对循环群进行 delooping
在 HoTT 中借助透镜空间构造循环群 Z_m 的胞腔式 delooping，推广实射影空间构造
近似问题的代数方法
为 valued promise CSP 建立代数框架，用 valued minion 同态统一导出近似归约与不可近似性。
目标化消息更有效吗？
回答 GNN 中依赖源与目标状态的消息版本是否比仅依赖源状态版本表达力更强，证明非一致设置下等价、一致设置下更强。
点深度三：J-类的回归
给出 BPol 算子的通用代数刻画，将高层成员问题归约到覆盖问题，并证明点深度三可判定。
组合代数中的辫、扭曲、迹与对偶
提出 ribbon 组合代数，证明其与 ribbon 范畴中自反对象对应，并给出迹与对偶两种等式刻画。
有限值流式字符串转换器
将经典有限值转换器的分解与判定结果推广到 copyless 流式字符串转换器，证明其有限值性可判定。
关系结构上的并发博弈：博弈余单子的起源
用事件结构统一构造 Spoiler-Duplicator 博弈余单子，并刻画一/双侧博弈策略。
有限结构上双向互模拟不变的一元最小不动点逻辑的刻画定理
证明有限结构上双向互模拟不变的一元最小不动点逻辑恰好对应双向 μ-演算。
通过 I/R 树的深度分析界定 Weisfeiler-Leman 维数
引入 WL 深度分析 I/R 分支树，证明计数一阶逻辑下定义 n 顶点图所需变量数的新上界。
论 Maslov 类 K̅ 的复杂度
证明 Maslov 类 K 具有指数模型性质，从而确定其可满足性问题是 NExpTime 完全的。
原始递归依赖类型论
通过限制 Martin-Löf 类型论的自然数消去与宇宙，构造 Tpr 理论，使可定义函数均为原始递归。
在一阶逻辑中定义算法呈现的结构
提出准可公理化概念，用一阶扩展语言中的∃/∀/∃∀/∀∃句刻画两类算法呈现结构的同构型。
秩递减转换
用割秩刻画 MSO 可定义转换：在有界树宽输入上，渐近降低割秩的转换恰为 MSO 可定义转换。
严格结合且单位的 ∞-范畴的语法
首次以类型论语法定义严格结合且单位的 ∞-范畴，并用 insertion 计算规则实现相等判定。
从整数类型构造自然数类型
仅用 Σ、Id、Π 与带大消去的二元素类型，从整数类型构造出自然数类型。
PCSP 的单射硬度条件
提出基于平滑分层 PCP 定理的单射硬度条件，据此证明一类 PCSP 模板 NP 难，并建立布尔线性阈值模板的二分定理。
有限随机结构的一阶复杂度
定义有限随机结构的一阶复杂度层级，引入随机 FO 归约，给出若干新逻辑极限律并证明 0-1 律句法集不可递归枚举。
稀疏随机图的一阶可区分性
证明稀疏随机图两份独立样本的一阶可区分量词深度取决于 α 的有理逼近，并给出上下界。
202366 篇 · 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
基于偏马尔可夫范畴的证据决策论
提出偏马尔可夫范畴，统一刻画带约束、观测与更新的随机过程，并形式化证据决策论。
概率编程的确定性流采样：语义与验证
提出以采样器为中心的高阶概率语言，给出操作/指称语义，并建立验证采样器正确性的演算。
ωPAP 空间：高阶、递归概率与可微程序的指称式推理
提出 ωPAP 空间范畴，为高阶递归概率与可微程序建立指称语义，并证明自动微分与密度计算等正确性。
带正则递归类型的自动摊销资源分析
为任意正则递归类型定义的代数数据结构构造资源多项式，并在 AARA 资源类型系统中实现复杂数据结构上的自动资源界推断。
可解释人工智能的逻辑
提出基于符号逻辑的可解释性语义与计算理论，从决策的必要/充分条件刻画解释。
自动化验证中的交换性
提出利用迹理论与交换性，将原验证任务替换为更简单的等价程序进行可靠验证。
论一阶逻辑二变量片段中的精确采样
证明 FO2 及其带计数约束扩展在采样意义下具有域可提升性，给出多项式时间精确采样算法。
论概率下推自动机中的证书、期望运行时间与终止性
揭示概率下推自动机证书存在性与期望终止时间的联系，并给出正几乎必然终止的易验证证明。
单射分段仿射映射的可达性
证明单射的一维两区间分段仿射映射可达性可判定，并揭示相关问题的丢番图与拓扑性质。
验证常速率多模式系统的线性时序规范
为常速率多模式系统引入 LTL 变体，并刻画其模型检测片段的复杂度版图：P-完全、NP-完全或不可判定。
图神经网络的描述复杂性
用描述复杂性与电路复杂性精确刻画图神经网络的表达能力，证明其对应守卫片段 GFO+C 与 TC0。
量子电路的完备等式理论
首次提出并证明量子电路的完备等式理论，使两个电路表示同一酉映射当且仅当可由这些等式互相变换。
任意有限维度下 ZXW 演算的完备性：一个统一的演算
把 ZXW 演算推广到任意有限维 qudit，并证明其完备性，是首个超越 qubit 的通用图形语言完备性结果。
计算线性包：判定域上加权自动机是否确定与无歧义
给出计算域上加权自动机线性包的算法，判定其是否等价于确定或无歧义自动机，并解决2006年公开问题。
面向定量目标的随机博弈值迭代停止准则
首次为带总收益和平均收益目标的随机博弈值迭代给出停止准则，并实现相应 anytime 算法。
DiLL 模型中作为单子的泰勒展开
为 DiLL 引入 codigging 规则，证明 ! 在范畴语义中构成单子，且每条证明等于其泰勒展开，模型因此定量。
面向密码推理的高阶不可区分逻辑
重新设计 SQUIRREL 的逻辑基础，提出高阶不可区分逻辑，支持通用推理与可扩展的密码协议验证。
QBF 的结构感知下界与可处理性视野的拓宽
为 QSAT 在关联图等结构参数下建立紧下界并给出新 FPT 算法，基本补齐其参数化复杂度图景。
在 Cubical Agda 中形式化 π₄(S³) ≅ Z/2Z 并计算一个 Brunerie 数
在 Cubical Agda 中完全形式化 π₄(S³)≅Z/2Z，并通过计算简化后的 Brunerie 数完成计算机辅助证明。
高阶数学操作语义中的弱相似性
在高阶 abstract GSOS 框架下证明弱相似性的同余定理，并实例化为 λ-演算的 applicative similarity。
集合论序数与类型论序数一致
证明在Aczel解释下，构造集合论序数与HoTT类型论序数等价，并推广到所有集合。
按值调用 PCF 的完全抽象正规形式双模拟
提出首个针对按值调用 PCF 的完全抽象正规形式双模拟，并实现有界检查工具。
Borel 目标下的随机尽力而为策略
证明任意 Borel 目标在未知非马尔可夫随机环境中存在支配序极大的随机尽力而为策略，并给出 LTL 合成复杂度。
高维子图匹配
在图表集合框架下研究高维图重写中的子图匹配问题，给出任意维匹配算法及其复杂度界。
带传递闭包的存在关系演算：复杂性与边饱和
本文用边饱和刻画 ECoR* 及其片段的等式理论，并确定其可判定性与复杂度。
中心子单子与计算概念：可靠性、完备性与内部语言
将中心性/中心子单子概念推广到对称幺半范畴上的强单子，并建立带中心子单子的λ演算语义的可靠性、完备性与内部语言结果。
群胚的 thin spans 笛卡尔闭双范畴
提出群胚的 thin spans 双范畴，并证明其 Kleisli 双范畴在伪余单子 ! 下是笛卡尔闭的。
群分离问题卷土重来
重新证明群语言分离与覆盖的可判定性，仅用自动机理论，并给出紧复杂度界。
单子二阶逻辑中的树量化
提出单子树逻辑 MTL，在无限树上对任意子树进行二阶量化，刻画其表达能力并联系分级 µ-演算与策略时序逻辑。
折叠解释
提出带 fold 迭代机制的组合子系统，并用线性逻辑启发的类型系统将其限制到恰好生成 polyregular 函数。
强化版 PDL：PDL 含交与逆的表达力扩展
提出逻辑族 CPDL+，严格包含 ICPDL、CQ/CRPQ 等，并用树宽刻画表达力层次及可满足性/模型检测复杂度。
半度量空间上的不动点逻辑
在更广的半度量空间上建立 wK4 及相关逻辑的度量完备性，并提出混合缠结以刻画 µ-演算的表达力。
2-范畴结构的不动点算子
将 Plotkin–Simpson 的不动点算子定理范畴化到 2-范畴，统一建模(共)归纳类型与执行步骤。
超越受限量词坍缩的嵌入式有限模型
重新审视嵌入式有限模型理论，扩展量词坍缩分析并比较签名与可判定理论。
幺半群上的动力系统最小化
提出广义前向双模拟及划分细化算法，统一并扩展动力系统在交换幺半群上的最小化。
操作式算法博弈语义
为带状态简单类型 CBPV 给出操作式博弈语义的全抽象迹模型，并用自动机识别可判定片段。
符号操作的寓言（Allegory）理论
提出基于 allegory 与范畴语法的通用关系式符号操作理论，统一并行移动与 Tait–Martin-Löf 技术。
伪随机有限模型
从逻辑可定义性角度研究伪随机有限结构，并分类哪些逻辑转换可作为伪随机生成器。
Positivity 的力量
证明实代数数上线性递推序列的正性问题可归约到整数上，并给出可对角化线性动力系统半代数模型检测的相对可判定性。
基于证明搜索的推理系统：扩展摘要
提出 PSF 证明搜索框架，给出其设计与元理论，并统一刻画经典、直觉主义与线性逻辑的证明系统。
Weisfeiler-Leman 算法的迭代次数
给出 k-WL 稳定迭代次数的上界 O(k n^{k-1} log n) 与下界 n^{Ω(k)}，并揭示维数与迭代次数的权衡。
分布式知识的半单纯集模型
将单纯复形推广为半单纯集，为分布式知识认知逻辑建立新语义并给出可靠完备公理化。
信息不等式在数据库理论问题中的应用
系统介绍信息不等式并展示其在查询输出上界、最坏情况最优连接、查询支配和近似完整性约束蕴含中的应用。
直觉主义 S4 的可判定性
通过双标签证明搜索，证明直觉主义模态逻辑 S4 可判定并获得有限模型性质。
论 Polyregular 函数的增长率
polyregular 函数输出规模 O(n^k) 当且仅当可由 k 维 MSO 解释定义，且 pebble transducer 无此刻画。
不能解释某个有限事物的图与结构的对称性
研究图与结构在无法pp解释所有有限结构时被迫满足的代数对称性，推广CSP可解性相关定理并构造无限反例。
从薄并发博弈到广义结构种（generalized species of structures）
在基于事件结构的薄并发博弈与基于分配子的广义结构种之间建立双范畴桥接，并获得笛卡尔闭伪函子。
面向代价感知指称语义的元语言
提出用于代价感知指称语义的元语言，为 STLC 与 Modernized Algol 构造合成模型并证明代价感知计算充分性。
布尔对称模板与函数式目标 PCSP 的二分性
证明布尔对称模板对函数式目标 PCSP 的二分性，并比较 BLP+AIP 与 AIP 的强度。
轨道有限线性规划
证明轨道有限线性不等式组的实数可解性与优化可判定，并证明整数版本不可判定。
让并发函数化
通过并发博弈与策略统一函数式与交互式计算，并表明多种函数式/逻辑方法是其全子范畴。
笛卡尔相干微分范畴
将相干微分从线性逻辑范畴模型推广到一般笛卡尔范畴，并给出可解释微分项语言的语义框架。
Max-Plus 自动机的 Big-O 问题是可判定的（PSPACE-完全）
证明 max-plus 自动机的 big-O（仿射支配）问题可判定，且为 PSPACE-完全。
Z² 上的特殊仿射群中的恒等元问题
证明 Z² 的特殊仿射群中有限生成半群的恒等元问题与群问题可判定且 NP 完全。
扩展与非扩展的函数作为进程
通过参数化 wires 细化 Milner 编码，统一刻画扩展与非扩展的函数作为进程 λ-理论。
重访有理关系子类中的成员问题
重新审视有理关系子类间的成员判定，改进复杂度并给出新的可判定性结果。
Cut-Restriction：从切割到解析切割
提出 Cut-Restriction，将任意切割限制为解析切割，在无法切消时恢复子公式性质并统一已有结果。
用对数级量词深度模拟对数空间递归
证明 LREC= 可定义性质可由 k 变量 FO+C 以对数数量词深度表达，并给出 Weisfeiler–Leman 对数轮数刻画。
带计数的二变量一阶逻辑对有根无秩树上一阶逻辑查询的表达完备性
证明有根无秩树上任意一元一阶查询都可在带计数的二变量一阶逻辑中表达。
逻辑中组合方法的范畴论刻画
用 game comonad 语义统一刻画有限模型论组合方法中的 FVM 型定理，并给出参数化构造。
代数级数与上下文无关文法上的重数问题
将代数幂级数的零性、有限支撑和系数计算归约到算术电路，改进了复杂度上界，并给出上下文无关文法重数等价等推论。
保持厄米性的超算子的通用完备图形语言
提出 ZW-calculus 扩展，为保持厄米性的超算子给出通用且完备的图形语言，支持反线性变换的图解研究。
ℤ-多正则函数
研究从有限词到整数的ℤ-多正则函数，给出逻辑、表达式、级数与转换器刻画，并判定其子类成员问题。
齐性假设下前缀与后缀逻辑（BE）是初等的
证明齐性假设下区间时序逻辑 BE 的有限可满足问题是 ExpSpace 完全的。
有界 twin-width 图的 distal 组合工具
证明有界 twin-width 图具线性邻域复杂度，并借助边关系 distal 获得 distal 切割与正则引理。
概率 Rabin 树定理
求解无穷树上一元二阶逻辑的概率满足问题：计算随机树满足公式的概率，并证明该概率为代数数。
202261 篇 · Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science
用于成本分析的量子期望变换器
提出混合经典-量子语言的期望变换器语义，可对量子程序做期望成本与期望值分析。
Curry 与 Howard 遇上 Borel
建立计数命题逻辑与概率事件 λ 演算的 Curry-Howard 对应，并以交集类型精确刻画概率行为。
超越定量代数推理中的非扩张运算
扩展定量等式逻辑以支持广义度量代数与提升意义下的非扩张运算，并公理化概率分布上的Ł–K距离。
具体范畴与高阶递归
提出一类具体层模型，统一概率与可微编程等语义，并证明通用计算充分性定理。
μ-演算中的规模度量与 α-等价
提出 α-不变的图表示，消除 μ-演算公式因绑定变量重命名导致的指数膨胀，并证明 Fischer-Ladner 闭包大小在 α-等价下不变。
超越上下文无关的概率验证
证明受限概率树栈自动机的几乎必然终止与ω-正则模型检测可判定，并对应概率 MAHORS。
定量代数的簇及其单子
证明可用 c-基本定量方程刻画的定量代数簇恰好是对应基本单子的单子范畴。
有界局部团宽图类的解释上的模型检测
证明在有界局部团宽图类的一阶解释类上，一阶模型检测存在 FPT 算法。
无限图上无限时长博弈中的位置性刻画
用通用图刻画无限图上定量无限时长博弈中允许最优位置策略的赋值，并证明与单调良序通用图存在性的等价（带中性颜色时）。
分级单子与行为等价博弈
提出从分级单子中提取通用 Spoiler-Duplicator 博弈，统一刻画不同粒度的行为等价，并引入无限深度分级语义。
固定维数 VASS 可达性问题的下界
为固定维数 VASS 的可达性问题给出四个改进的复杂度下界，覆盖 4 到 8 维的不同变体。
定量相等的逻辑基础
在 Linear Logic 中把距离视为相等谓词，用 graded modality 建立定量等式的证明系统与 Lipschitz doctrine 语义。
面向数据流编程的幺半流
将因果流函数推广到幺半范畴，为以对称幺半范畴表示过程的数据流语言与信号流图提供语义。
时序团队语义再探
重新审视时序团队语义，提出三种量化时间求值函数的异步 hyperproperty 逻辑，并分析其可判定性。
时间自动机局部时间语义的抽象：偏序方法的基础
为时间网络可达性提出局部时间语义下的抽象与包含检测，奠定偏序方法基础。
带有确定性状态子单子的概率单子
为概率单子引入sober对象与sobrification函子，并强化Markov范畴的de Finetti定理
连续特征的可计算 PAC 学习
在可计算度量空间上定义二分类可计算 PAC 学习，刻画 ERM 可计算性，并给出无可计算 proper 学习器的反例。
Valence 系统中双向可达性的复杂度
刻画 Valence 系统双向可达性的复杂度，证明多数可判定存储机制下复杂度降至多项式时间。
线性算术理论的几何判定过程与 VC 维
给出 LIA 的三重指数几何判定过程，并证明其可定义集 VC 维的双重指数上界，解决 Nguyen–Pak 猜想。
SAT 解的几乎均匀生成：3-独立哈希的威力
提出基于3-独立哈希的SAT解几乎均匀生成算法，在562个基准上全部成功而JVV超时544个。
结合 n-范畴的 Zigzag 规范化
提出结合 n-范畴项规范化的 zigzag 构造算法，证明其正确性，并用于证明助手 homotopy.io。
线性逻辑的线性代数模型：作为 Σ-半环上模范畴
提出以 Σ-半环上模范畴统一线性逻辑的线性代数模型，并得到带余自由指数的直觉主义线性逻辑模型。
自动结构上的 Ramsey 量词：复杂度及其在验证中的应用
研究自动结构上有向 Ramsey 量词的复杂度，建立 NL 至 EXP 图景，并用于验证问题。
工作流网中健全性的复杂度
确定了工作流网三类健全性判定问题的精确复杂度：经典与结构健全性为 EXPSPACE 完全，广义健全性为 PSPACE 完全。
具有子词序的上下文无关字符串约束的可满足性
证明带子词序的上下文无关字符串约束一般不可判定，无环依赖片段为 NEXPTime 完全，并确定无环有损通道下推系统控制状态可达性的复杂度。
代数几何与线性逻辑之间的函子式漫游
用函子点方法为交换环上的预层（含 scheme）构造预层模范畴，并证明其构成直觉主义线性逻辑模型。
λμ-演算的资源近似
将 Taylor 展开适配到 λμ-演算，建立资源敏感近似理论，并证明稳定性与垂直线性质。
从正则转换器表达式高效构造可逆转换器
提出首个初等过程，将正则转换器表达式高效构造为等价的二向可逆转换器，并给出双指数/指数复杂度上界。
λ演算的合理空间：对数级
提出基于Krivine抽象机变体的λ演算空间代价模型，首次支持对数空间，并研究其时间行为与call-by-value移植。
令人惊奇的混合多项式闭包及其在二变量一阶逻辑中的应用
提出混合多项式闭包 MPol，证明其保持成员与分离可判定性，并用于 FO2 量词交替层级。
具有同步目标的随机博弈
研究随机博弈中同步目标的获胜分布，给出算法并确定判定问题的 PSPACE/PTIME 完全性。
通过 update recursion 对二阶算术的直接计算解释
用 update recursion 直接解释二阶算术的二阶消去，弥合 bar recursion 与多态 λ 演算两条计算解释路径。
面向可靠确定型协商的主动学习
为可靠确定型协商提出两种主动学习算法，利用其结构实现最小化，查询复杂度与协商规模多项式相关。
光滑逼近与有限有界齐次结构上的 CSP
提出光滑逼近技术，统一证明随机锦标赛等齐次结构上 CSP 的二分类，并刻画局部一致性可解性。
有限模型论中的 pebble-relation 余单子
引入 pebble-relation 余单子，用余Kleisli 映射刻画 k 变量无穷逻辑受限合取片段，余代数对应 pathwidth 与路径分解。
循环与非良基证明中的弹跳线程
提出 bouncing-validity 广义有效性判据，使含公理与切的循环/非良基证明可组合，并证明可靠性与切消。
论 Skolem 问题与 Skolem 猜想
证明可逆 7 阶及以下线性递推序列的 Skolem 问题可判定，并在 Skolem 猜想下给出 5 阶判定过程。
多项式增长的换能器
综述 polyregular 函数（多项式规模输出的字符串函数）的五种等价定义、判定问题与受限子类。
用于推理量子程序期望运行时间的量子最弱前置条件
将期望运行时间定义为量子最弱前置条件的推广，给出有限维量子程序期望运行时间计算方法并解决量子随机游走开放问题。
半环语义下一阶逻辑的零一律与几乎必然赋值
将随机结构上一阶逻辑的零一律推广到半环语义，并刻画有限格半环中语句的几乎必然赋值及计算复杂度。
Greatest HITs：通过时钟下的归纳在余归纳定义中的高阶归纳类型
提出 Clocked Cubical Type Theory，结合多时钟守卫递归与立方类型论，并用时钟下归纳编码余归纳类型。
Milner 关于正则表达式模双相似性的证明系统是完备的
证明 Milner 1984 年提出的正则表达式进程语义双相似性证明系统完备，并引入保持 LLEE 的结晶化程序处理空步图。
判定与功能规约相结合的超性质
系统研究 ∀*∃* HyperLTL 的可满足性片段，并分析其与 LTL 功能规约组合后的可判定性与复杂度。
严格单位 ∞-范畴的类型论
用类型论刻画带严格单位的 ∞-范畴，给出定义相等性的归约判定过程，并证明严格单位性是性质而非结构。
稀疏图转导的树状分解
为稀疏图类的一阶逻辑转导建立树状分解定理，并解决 low-shrubdepth 覆盖的开放问题。
循环隐式复杂度
通过基于 safe-normal 函数代数的循环证明系统，用证明论约束刻画多项式时间与初等可计算函数，连接循环证明与隐式计算复杂度。
模电路（modular circuits）的复杂性
研究模电路计算 AND 的复杂度及其可满足性分类，并应用于有限群方程求解。
数值域上的数据词推理
提出带参数与Presburger约束的数据词逻辑pSDL，支持数值算术与数据计数，并给出可判定性和复杂度。
非负有理数上加权自动机的有界性与零隔离问题
证明无复制线性加权自动机有界性可判定，并把零隔离归约到正交向量加法系统，三维情形在 Schanuel 猜想下可判定。
轨道有限（orbit-finite）线性方程组的可解性
在原子集合框架下给出轨道有限线性方程组可解性的判定过程，并证明其生成向量空间具有轨道有限基。
论 Sherali-Adams 与 Nullstellensatz 作为命题证明系统的强度
刻画 Sherali-Adams 与 Nullstellensatz 相对于 Frege 类系统及树状/一般 Resolution 的证明强度。
同伦类型论中的 Syllepsis
在 Martin-Löf 类型论中，利用 intensional identity type 的消去规则构造出 syllepsis 一致性单元。
无元素概率论中的划分与 Ewens 分布
用基于多重集的无元素方法重构 Ewens 分布理论，提出划分多项式定理与无元素多项分布。
二维类型理论的语义
提出 comprehension bicategories 作为二维类型理论的一般模型，统一并涵盖已有的 directed type theory 解释。
根式表达式的恒等测试
证明根式恒等测试在 GRH 下属于 coNP，且平方根素数版本在 GRH 下属于 coRP、无条件属于 coNP。
分离 LREC 与 LFP
证明 LREC 严格弱于 LFP：路径系统问题在 LFP 可定义但 LREC 不可定义。
经典可实现性中特征布尔代数的一阶完备性结果
证明任何至少含两个元素的布尔代数都可由某个 Krivine 风格经典可实现性模型的特征布尔代数初等等价表示。
有界 twin-width 的稳定图
证明单调稳定且有界 twin-width 的图类可由有界稀疏 twin-width 的图类经 transductions 得到，并推出线性 χ-有界性。
带见证对称选择的无选择多项式时间
通过引入带见证对称选择扩展 CPT，使可定义同构自动蕴含可定义规范化，并在同构可定义结构类上自动捕捉 Ptime。
带一次交替的一阶逻辑的正则语言
证明带中性字母的 Σ₂ 正则语言可由仅用序关系谓词的 Σ₂ 公式定义，推进 Straubing 中心猜想。
当局部性与保持性相遇
刻画 Gaifman 正规形中局部句子的正布尔组合，证明其恰好对应局部初等嵌入下保持的一阶句子。
202193 篇 · 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
一种面向条件独立性的束逻辑
扩展 BI 逻辑以非交换合取刻画条件独立，并基于 Markov 核与幂集单子给出模型和概率程序验证逻辑。
随机 λ-演算的通用语义
为随机 λ-演算建立可靠且充分的指称语义与操作语义，统一高阶概率程序的语义框架。
带精确条件化的概率程序的组合语义
为带一阶精确条件化的高斯概率程序建立操作、指称与等式语义，并用范畴构造 Cond 推广精确条件化。
基于操作博弈语义的组合式关系推理
提出 Kripke 范式双模拟，用操作博弈语义统一四类高阶语言的上下文等价关系推理，并证明其可靠完备。
上鞅、秩函数与概率 λ 演算
提出基于秩上鞅的概率λ演算几乎必然终止证明方法，并给出反单调、稀疏与替代归约策略下的扩展。
局部完全抽象解释的逻辑
引入局部完全性，并给出证明系统，首次结合过近似与欠近似以同时证明程序规范的正确性与不正确性。
面向概率编程语言的可交换单子
在 DCPO 范畴上构造三种概率可交换单子，并为概率不动点演算给出可靠且充分的指称语义。
结合非确定性、概率与终止：等式推理与度量推理
给出非确定性、概率与终止组合所得 monad 的呈现，提供程序等价性与距离的等式推理工具。
Perspective 多玩家博弈
将 Perspective 博弈扩展到多玩家、联盟与非零和，证明不可判定边界，并给出两人非零和可判定与理性合成结果。
从分布上的多重集到多重集上的分布
本文构造并刻画多重集单子到分布单子的分配律，统一非确定性与概率语义并应用于采样语义。
通过耦合与 up-to 方法高效局部计算微分双模拟
提出多项式耦合与局部算法，高效计算多项式微分方程上的微分双模拟等价，并支持 up-to 技术与负例约束。
责任与验证：时序逻辑中的重要性值
将 Shapley 值引入模型检测，度量系统组件对满足时序规约的重要性，并给出线性与分支时序逻辑下的复杂度上下界。
基于构造性实数的全局优化
在构造类型论与可计算实数下建立全局优化与回归的联系，并给出收敛准则及 Agda 机器化证明。
关系霍尔逻辑的对齐完备性
提出对齐完备性概念，用归纳断言法与乘积自动机刻画关系霍尔逻辑的规则完备性。
定量等式逻辑的不动点
为定量等式逻辑引入不动点扩展，在定量代数中给出近似相等语义，并刻画收敛速率与 Conway/迭代理论。
概率验证中的符号时间与空间权衡
提出更快的符号算法计算 MDP 的最大端分量分解，给出符号操作与空间权衡，解决长期开放问题。
HyperLTL 的异步扩展
提出 HyperLTL 的两种异步正交扩展 HyperLTLS 与 HyperLTLC，证明一般模型检测不可判定并给出可判定片段及复杂度。
Bunched Logic 的量子解释与量子分离逻辑
提出 Bunched Logic 的量子模型，并构建量子分离逻辑以验证量子程序安全性。
网的范畴
提出 Σ-网统一 Petri 网及其变体，并用左伴随函子刻画其执行语义与相互嵌入。
面向非干涉的会话逻辑关系
提出面向线性会话类型的信息流控制类型系统，并用按保密级别索引的会话逻辑关系证明非干涉性。
面向更高效的双变量逻辑可满足性方法
将双变量逻辑可满足性归约为条件独立集问题，并给出首个显著优于 O(2^{2n}) 的确定/随机算法。
一阶逻辑的组合证明与分解定理
揭示一阶逻辑组合证明与句法证明的关系，通过深度推理分解定理给出新正规形式及可靠/完备/完全完备性结果。
交互的空间
提出树交集类型系统，精确刻画交互抽象机的空间消耗，并重新审视λ演算的合理空间猜想。
立方类型论的归一化
证明了（单值、笛卡尔）立方类型论的归一化，得到无归约的范式双射，并推出判断相等的可判定性与类型构造子单射性。
没有 Beth 与 Craig 也能生存：守卫片段与二变量片段中的定义与插值
证明守卫片段和二变量片段中插值与显式定义的存在性可判定，并刻画其复杂度。
单子重写系统的关系理论（第一部分）
提出单子重写的关系理论，识别弱笛卡尔单子与线性方程条件，并给出带代数效应的 CBV λ 演算的标准化与合流定理。
用数据自动机验证高阶并发程序
用分离控制与内存的 split 自动机编码 FICA，并为高阶并发找到一个验证可判定片段。
面向归约主义者的 System F 可类型性与类型检查不可判定性
给出从半统一到 System F 可类型性的直接归约，简化经典不可判定性证明并在 Coq 中机器验证。
一阶推理与高效半代数证明
为一阶理论刻画常次代数与半代数证明系统，并给出分离及命题证明新结果。
初始极限 Datalog：一类新的可扩展可判定约束霍恩子句
提出初始极限 Datalog，将可判定极限 DatalogZ 推广到高阶并支持任意合适背景理论。
通用 Skolem 集
引入并构造出通用 Skolem 集，使线性递推序列的零项判定在一类无限下标集合上可有效进行。
交类型分配子
构造 distributor 诱导的双范畴模型，为 λ-演算提供交类型系统的 proof-relevant 语义并刻画可解性。
有限结构上的约束满足问题
系统研究含关系与运算的有限结构上 CSP 的计算复杂度，给出代数条件并完成二元素结构分类
连续单计数器自动机
证明连续单计数器自动机可达性：全局界测试在 NC²，一般情形多项式时间，参数化情形在多项式层级内可判定。
三守卫片段及相关逻辑的有限模型论
证明三守卫片段具有有限模型性质，并确定其及相关带传递守卫片段的有限可满足性复杂度。
加权一元二阶逻辑的公理化与可计算性
为加权一元二阶逻辑及其无一般和片段给出完备公理化，并分析相关判定问题的可判定性与不可判定性。
一种带经典证明与反驳的构造性逻辑
提出区分肯定/否定与强/经典四模态的经典命题逻辑保守扩张，并给出自然演绎、Kripke语义与项赋值系统。
高效布尔 Skolem 函数合成的范式刻画
提出 SAUNF 范式，精确刻画布尔 Skolem 函数何时可多项式时间合成及何时有多项式大小解。
具有普通复合的关系半群中的 demonic 格与半格
研究带普通复合与 demonic 格运算的关系半群，揭示其表示类的有限公理化与可判定性边界。
移除冗余拒绝：失败迹语义下的最小完备测试套件
为失败迹语义提出生成最小完备测试套件的方法，通过基本拒绝与枚举去冗余。
具有公式不动点的线性逻辑的范畴模型
为带最小/最大不动点的命题线性逻辑 μLL 建立范畴语义，给出两个模型，后者展示指称式证明归一化。
λ-演算的组合式代价模型
基于博弈语义为按值调用 λ-演算提出组合式时间代价模型，并在 RAM 上给出保常因子的完全惰性图归约实现。
定量与近似监控
将运行时验证推广为对数值 trace 属性进行近似估计的定量监控，并刻画精度-资源权衡。
π 演算中的顺序性与良括号性
用类型系统刻画顺序性与良括号性，并给出比普通互模拟更粗的标号互模拟，证明其可靠性与受限完备性。
定量模态逻辑的表达力：基于余密度与近似的范畴论基础
提出基于余密度提升与近似族的范畴框架，统一推导定量模态逻辑的表达力结果。
2001年Test-of-Time Award获奖引文
公布2021年LICS 2001测试时间奖，表彰两篇发表于LICS 2001的论文。
无界输入程序的差分隐私线性时间可判定性
提出自动机模型，并证明无界实数查询答案输入程序的差分隐私可在线性时间内判定。
字上的正一阶逻辑
给出 Lyndon 保持定理在有限结构上失败的简单证明，并证明正则语言的 FO+ 可定义性不可判定。
平方和与多项式演算中单项式大小与比特复杂度
构造布尔约束Q_n：存在度2且单项式数多项式的SOS/PCR/ℚ反驳，但任何反驳均需指数级比特复杂度。
从有限值非确定性转换器到确定性双带自动机
刻画有限值、函数型、无歧义非确定性有限转换器的关系何时可由确定性双带自动机验证，并证明判定不可判定。
守卫片段（guarded fragments）的余单子语义
用资源索引余单子统一刻画量词守卫一阶逻辑片段的模型比较游戏，并用余代数对应守卫树分解。
拓扑 μ-演算：完全性与可判定性
为拓扑 μ-演算建立完全性、可判定性与有限模型性质，并给出关系 μ-演算自然片段的通用完全性结果。
可逆素事件结构的分布式操作视角
给出可逆素事件结构的操作刻画，并证明其对应于一类可逆因果网。
论简单类型 λ 演算的广义度量空间
提出基于广义逻辑关系的定量语义，构造笛卡尔闭的广义度量空间范畴，将欧氏度量扩展到高阶类型。
具有有限模型性质的一些构造性 S4 变体
证明了 CS4 具有有限模型性质，并引入 GS4 与 S4I，证明三者均具有有限模型性质。
到一阶逻辑性质的消除距离的参数化复杂度
刻画了到一阶逻辑可定义图性质的消除距离问题的固定参数可解性边界：Σ3 公式可 FPT，Π3 公式则 W[2]-难。
带延迟迹的图语言：用有限内存描绘量子计算
提出延迟迹的图语言构造，将任意可丢弃图语言扩展为有限内存计算语言，并给出流语义及完备性结果。
数据集成中的抽象
首次系统研究数据集成中的“抽象”问题：给定源模式上的查询，求其在全局模式上、模映射等价地刻画原查询的抽象查询，并给出形式化框架与研究展望。
图神经网络的逻辑
用有限变量计数逻辑与 Weisfeiler-Leman 算法精确刻画图神经网络的表达能力。
轨道有限维向量空间与加权寄存器自动机
提出轨道有限维向量空间理论，并据此给出加权寄存器自动机等价性的判定过程，复杂度指数时间、固定寄存器数多项式时间。
多结构博弈与量词数量
提出多结构博弈，以 r 轮胜负刻画分离两组结构所需一阶量词数，并完整判定线性序区分所需量词数。
论同态计数的表达能力
研究右同态轮廓限制可刻画哪些图同构松弛，揭示左右轮廓表达力显著差异。
Evidenced Frames：一个拓宽可实现性模型的统一框架
提出 Evidenced Frames 框架，统一并拓宽可实现性模型，使 realizer 本身可带状态、非确定性与失败等效应。
假设恰好足够的公平性使会话类型对无锁性完备
系统刻画公平性假设下的三种无锁性语义，并给出仅假设 justness 时完备的会话类型系统。
依赖类型理论的内部 ∞-范畴模型：迈向 2LTT 吞食 HoTT
提出 ∞-CwF，在二层级类型论中为无 UIP 的 HoTT 提供内部依赖类型论模型。
异步模板博弈与 2-范畴的 Gray 张量积
将模板博弈提升到 2-范畴，用 Gray 张量积刻画异步并发，并给出 MALL 的异步模板博弈语义。
弱化与收缩超序列子结构逻辑中的可判定性与复杂度
证明了具有无割超序列演算的所有 HFLew 解析结构规则扩张可判定，并给出弱化与收缩扩张的复杂度上界及 MTL 的首个复杂度界。
Lovász 型定理与博弈余单子
提出一个范畴化 Lovász 定理，统一 Weisfeiler-Leman、计数逻辑与树深度等同态计数刻画，并给出模态逻辑新应用。
稀疏一般值 CSP 的 PTAS
将稀疏图上有限值 Max-CSP 的 PTAS 推广到含严格约束的一般值 CSP，并刻画对角化条件。
强传值调用是合理的：内爆式共享
提出新抽象机证明强传值调用求值合理，开销线性并以内爆式共享实现指数加速。
有限状态行为上发散保持分支同余的完备公理化
为有限状态行为提出保持发散分支同余的完备等式公理化，解决1993年以来的公开问题。
最小 Taylor 代数：CSP 三种代数方法的共同框架
通过本原正可定义性定理与最小 Taylor 代数，统一并简化 CSP 三种代数方法，为二分定理提供新框架。
论逻辑与同态闭包
系统研究逻辑句子模型类的同态闭包问题，并刻画一阶与二阶逻辑多片段的计算性质。
带计数的固定点逻辑中 Unique Games 的不可近似性
证明在 FPC 中无法近似 Unique Games 最优值，并给出两类新的不可近似性结果。
禁用诱导子图与 Łoś–Tarski 定理
证明有限图上 Łoś–Tarski 式的禁用诱导子图刻画失效，且该刻画不可计算、大小无界。
高阶透镜
在 HoTT/单价基础中提出高阶透镜，解决传统良行为透镜在证明相关设置下失效的问题，并刻画其性质。
论选择与 bar induction 原则的逻辑结构
提出广义依赖选择 GDC 与广义 bar induction GBI，统一刻画多种选择、bar induction 及相关逻辑原则的强度。
带 neighbour 关系的一阶逻辑的代数刻画
用对合半群及其局部 Hermitian 积刻画有限字上带 neighbour 关系的一阶逻辑，并建立 Eilenberg 型对应。
参数性与半立方类型
从任意类型论模型构造出满足参数性的模型，并揭示参数性与半立方类型的对应。
Monoidal 理论的 Smash 乘积
将 props 的张量积推广为带点有向空间的 smash 乘积，统一 monoidal theories 并生成高维 coherence 数据。
可证性逻辑的零一律：在几乎所有模型和几乎所有框架中公理化有效性
证明可证性逻辑的模型与框架零一律，并分别公理化其几乎必然有效公式。
面向非周期变换的 SD-正则转换器表达式
用受限 Kleene 星的 SD-正则转换器表达式刻画一阶可定义函数，推广 Schützenberger 的 SF=AP 结果。
Ramsey 结构的典范多态与唯一插值性质
给出将这类无限域 CSP 归约到 k-型有限域 CSP 的充分条件，并用于证明 RCC5 一阶扩展的新复杂度二分。
Laplace 机制对连续查询的差分隐私具有最优效用
证明在连续查询的差分隐私中，Laplace 机制在给定隐私约束下达到最优效用，推广了离散情形的几何机制最优性。
Heyting-Lewis 蕴涵的 Gödel-McKinsey-Tarski 与 Blok-Esakia
为 Heyting-Lewis 逻辑建立描述性框架对偶，并借经典模态翻译证明 Blok-Esakia 定理与可判定性。
无限字母表上的 Parikh 定理
证明单寄存器自动机/文法语言的交换像总是有理的，并指出未必半线性，猜想多寄存器情形类似。
寻找失去的时间：进程代数中并行组合的公理化
综述并推进 CCS 并行组合公理化：解决有限可公理化边界及 rooted weak bisimilarity 无有限完全公理化等开放问题。
基于分级单子的行为预序
提出以 Pos 上分级单子统一刻画行为预序及其特征逻辑的语义框架。
类型是内部 ∞-群胚
通过多项式单子与 opetopic 类型，在类型论内部定义 ∞-群胚，并证明其与类型宇宙等价。
Lacon- 与 Shrub-分解：有界扩张类一阶转导的新刻画
引入 lacon- 与 shrub-分解，刻画有界扩张图类的一阶转导，并给出其 FO 问题线性时间可解的条件。
分离秩逻辑与多项式时间
证明 CFI 图在 Z_{2^i} 上的同构问题不可由秩逻辑定义但可由 CPT 定义，从而分离秩逻辑与多项式时间。
No-Rainbow 问题与满射约束满足问题
证明 No-Rainbow Problem 是 NP 难的，并推翻 SCSP 与带常量 CSP 复杂度等价的猜想。
从算法设计推导复杂性下界
综述如何利用算法设计进展，系统地证明电路复杂性等下界。
202070 篇 · Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science
判定具有有限输入和输出的程序的差分隐私
针对有限输入输出程序，研究差分隐私判定的可判定性，填补逻辑与统计方法回避的基础问题。
有限森林上带复合算子的模态逻辑
证明有限森林上两种带复合算子的模态逻辑的表达力与可满足性复杂度，并解决相关公开问题。
通过弱分配律组合概率选择与非确定性选择
证明幂集单子到有限分布单子存在弱分配律，导出凸幂集单子，并应用于概率-非确定系统的迹语义与行为等价。
调和非干涉与渐进类型
研究如何调和信息流控制中的非干涉与渐进类型，以恢复动态渐进保证。
线性时序逻辑与极弱交替自动机的一种高效规范化过程
提出LTL的直接语法规范化过程，得到单指数爆炸的范式，并用于构造确定性Rabin自动机。
论程序分支时间性质验证的逻辑方法的可计算性
揭示多数将分支时间验证归约为逻辑问题的进路，其逻辑问题严格难于验证问题，唯一例外是带不动点的一阶算术有效性。
有限域上概率程序的通用等价与多数性
研究有限域上概率程序等价的可判定性与复杂度，证明通用等价可判定并给出双指数上界。
在马尔可夫决策过程中混合概率与非概率目标
研究MDP中布尔组合的概率与非概率ω-正则目标，给出策略存在性算法和复杂度界。
不完美信息 ATL 的 Hennessy-Milner 定理
为不完美信息 ATL 建立基于历史的交替互模拟与共同知识语义之间的完整 Hennessy-Milner 定理，并证明相关互模拟不可判定。
词典序格结构上的一个不动点定理
提出词典序格结构上的不动点定理，统一非单调形式体系的最小不动点语义。
自动机学习
提出泛范畴框架，将多种语言的学习归约为代数自动机学习，并推广 Angluin 的 L* 算法。
面向可扩展近似模型计数的稀疏哈希
设计稀疏哈希函数，以更小概率选变量生成短 XOR 约束，提升近似 #SAT 模型计数的可扩展性。
面向认证抽象层的基于精化的博弈语义
提出融合博弈语义、精化演算与代数效应的统一框架，以嵌入并组合经机器验证的抽象层及证明。
双立方集合中有向单值性的构造性模型
在双立方集合中构造有向类型论的构造性模型，并用 Agda 形式化有向单值性。
作为高阶归纳类型的整数
在 HoTT 中用高阶归纳类型表示整数，避免集合截断并验证其与带符号自然数表示等价。
自动结构
回顾自动结构概念的起源与早期发展，追溯逻辑理论的自动机判定程序思想。
广义可达性随机博弈的值的近似
提出一种 anytime 算法，能以给定精度逼近广义可达性随机博弈的 Pareto 前沿并给出误差界。
Monad 与 Comonad 的交互定律
提出函子-函子与 monad-comonad 交互定律，统一刻画带效应计算与效应机器行为的交互，并联系有状态 runner。
面向经典逻辑的消耗类型与持久类型
提出消耗与持久类型系统，无需求值即可精确预测带控制算子函数式程序到范式的步数与范式大小。
一种基于层级类型系统、刻画可行泛函的类型化编程语言
提出带 oracle 调用的命令式语言与可判定层级类型系统，刻画基本可行泛函 BFF2。
交集类型的故事
综述交集类型自 20 世纪 70 年代以来的发展及其在语义、验证、综合与语言表达力等方面的应用。
大型与无穷商归纳-归纳类型
为大型与无穷 QIIT 建立元理论，并用 CwF 代数模型给出语义。
同伦类型论中的序列余极限
在 HoTT 中形式化证明序列余极限与 Σ-类型可交换，并推出若干推论。
向量加法系统（VASS）中正则可分离性的一种方法
研究 VASS 语言的正则可分离性，并讨论一维、覆盖、整数与交换 VASS 等可判定子类。
VASS 终止复杂性的高效分析
证明带恶魔非确定性的 VASS 的终止复杂性是否属于固定 Grzegorczyk 层可在多项式时间判定，并揭示层级增长间隙。
锥作为直觉主义线性逻辑的模型
证明锥与线性 Scott 连续函数范畴构成直觉主义线性逻辑模型，并定义张量积与指数对象。
概率事件流上的空间高效查询评估
开启概率字符串上查询的流式空间复杂度研究，用概率分布序列建模流数据不确定性。
使 Streett 确定化达到紧界
改进了 Streett 自动机确定化的状态复杂度，并证明匹配下界，使其达到紧界。
概率 λ 演算中非惰性的优势
研究概率 λ 演算中非惰性归约对概率应用双模拟与上下文等价关系的影响。
下推系统的互模拟有限性是初等的
证明若下推系统互模拟等价于有限系统，则存在规模初等有界的有限等价系统，从而该判定问题是初等可判定的。
简单类型理论的代数模型
将泛代数扩展为同时支持代数排序与变量绑定的框架，为简单类型理论提供代数模型。
不动点逻辑中的时态约束满足问题
证明时态 CSP 在 Datalog 与（计数/秩）不动点逻辑中的可表达性，并给出完整分类，表明有限域 Maltsev 条件无法推广。
动态数据竞争预测的复杂性
系统刻画动态数据竞争预测问题的计算复杂度，识别难解性来源与可高效求解条件。
将高阶归纳类型构造为群胚商
证明所有有限 1-截断高阶归纳类型都可由群胚商构造，并在 Coq/UniMath 中形式化。
并发分离逻辑遇上模板博弈
揭示并发分离逻辑与差分线性逻辑模板博弈语义的范畴联系，并据此重构 CSL 的异步交互解释。
一阶树到树函数
证明一阶和 MSO 可定义的树到树变换具有分解定理：均可由基本变换经函数复合等组合子生成。
Contextual Types 解析
综述 Contextual Types 的起源与能力：将类型与类型上下文配对，用于刻画部分程序、机器化元理论与元编程。
通过良基性实现连贯性
提出环归纳原则：若图是局部合流且（余）良基关系的对称闭包，则验证空环与局部合流环即可证明所有环的性质。
单时钟定价时间博弈是 PSPACE-难的
证明单时钟定价时间博弈的值计算是 PSPACE-难的，即使限制在树宽为三的 DAG 上，并给出树等受限类的多项式算法。
有界树宽 QBF 的下界
基于 ETH 证明按树宽和量词秩参数化的 QSat 需要 i 重指数时间，覆盖整个多项式谱系。
1-free 正则表达式模互模拟的完备证明系统
为 1-free 正则表达式建立模互模拟的完备证明系统，解决 Milner 开放问题的一个受限情形。
实数计算与概率独立性逻辑的描述复杂性
引入分离分支 BSS 机，给出其 NP 的 Fagin 型逻辑刻画，并用于概率独立性逻辑的数据复杂性。
消解有限不确定性
利用动态方法在相干/几何逻辑中以证明树的有限分支消解理想对象，证明非确定性相继式的语义保守性。
细胞式 Howe 定理
在范畴框架中定义替换封闭互模拟，并用 Howe 方法证明其同余性。
QBF 归结的硬度刻画与大小-宽度下界
用量化布尔公式的电路复杂度紧刻画 QBF 归结证明大小，提出决策表模型并给出大小-宽度下界。
常数深度代数证明的惊人能力
关注 AC0[p]-Frege 超多项式下界这一开放问题，讨论常数深度代数证明系统的能力与已有子系统下界。
超越公式的逻辑
提出直接在图上推理的证明系统，用模块分解与深推理证明 cut 可容许，并保守扩展 MLL+mix。
前法西斯理论中的俄罗斯构造主义
为 CIC 给出纯语法的 presheaf 模型，同时保持转换并解释完整依赖消去。
作为 dialgebra 逻辑的模态直觉主义逻辑
提出 dialgebra 对偶框架，将一大类模态直觉主义逻辑及其框架实例化，并给出完备性与表达性结果。
多正则（polyregular）函数的 Pebble 最小化
证明多正则函数正则当且仅当输出至多线性增长，并以输出多项式次数精确刻画所需 Pebble 数。
扩展 Kripke 引理与超矢列子结构逻辑的可判定性
通过扩展 Kripke 引理并内化收缩，证明所有具有无割超矢列演算的 FLec 公理扩张可判定。
双范畴笛卡尔闭结构的相干性与求值规范化
给出笛卡尔闭双范畴相干性的两种证明，将高维结构构造归约到一维范畴论。
Good-for-games ω-下推自动机
引入 good-for-games ω-下推自动机，其非确定性可沿运行消解，从而支持与博弈、树及其他自动机组合。
高阶结构同一性原理
将结构同一性原理推广到广泛的高阶范畴结构，并用双层次类型论与 FOLDS 签名刻画不可区分性。
有序抽象概率的一种刻画
通过 effect monoid 刻画实数单位区间，说明其结构可由少量合理假设自然导出。
论 Zorn 引理的计算内容
通过Gödel函数解释为有限类型算术中的Zorn引理抽象实例给出计算解释，并引入非良基偏序上的新递归形式。
带极值约束的寄存器自动机及其在二变量逻辑中的应用
提出带极值约束的无限树寄存器自动机，证明其空性问题可判定，并用于二变量逻辑。
模电路可满足性中的中间问题
研究同余模簇上电路可满足性分类中 nilpotent 但非 supernilpotent 代数的未决中间情形。
双无限词上正则关系的一致化
证明判定双无限词上给定 MSO 可定义关系是否存在同定义域的 MSO 可定义函数是可判定的。
当可达性遇到 Grzegorczyk
证明向量加法系统/ Petri 网的可达性问题属于原始递归复杂度类，即位于 Grzegorczyk 层级之内。
计数有界树深度同态
证明两个图的计数一阶逻辑量词秩≤k等价，当且仅当它们在树深度≤k的图上同态计数不可区分。
括号的重配对
研究 Dyck 词上擦除配对括号的一人游戏，并以“宽度”衡量策略代价。
一种可扩展存储的演算
提出可扩展存储的演算，为带全局环境的 call-by-need 抽象机及其 CPS 翻译提供形式化基础。
论有限群的Weisfeiler-Leman维数
为有限群定义三种Weisfeiler-Leman算法，刻画其表达能力与计数逻辑、双射石子博弈的关系。
ω-正则语言的扩展
证明在 ω-字上添加含中性字母的非 ω-正则语言会使 MSO 扩展不可判定。
n-截断类型论中的部分 univalence
在 n-截断类型论中研究部分 univalence，并解释其与 UIP 不相容的根源。
有界度类上的后继不变一阶逻辑
研究有界度结构类上后继不变一阶逻辑的表达能力。
有限 N^d 集合上受控坏序列的复杂度
给出 N^d 有限集合在 majoring 与 minoring 序下受控坏序列长度的上下界，并转化为 fast-growing 复杂度类界。
通用代数上的隐藏子群问题
将隐藏子群问题推广到任意代数结构，并对二元代数幂的量子/经典可解性给出完全分类。
论具有有界严格宽度的有限有界齐次二元核的一阶扩张的关系宽度
研究具有有界严格宽度的有限有界齐次二元核的一阶扩张的关系宽度，推进关系宽度有界性分类。
201964 篇 · 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
贝叶斯编程的交互几何
为带连续采样与软条件的高阶贝叶斯 λ-演算建立交互几何模型，并证明其对两类操作语义充分。
基于度量的概率关系推理
扩展 Fuzz 以支持概率程序的一般关系性质，并用范畴语义刻画概率散度组合，覆盖近似差分隐私。
概率函数式程序的基于类型的复杂度分析
提出 λRPCF 类型系统，通过动态分布类型与 Lyapunov 秩函数，对概率高阶函数式程序进行组合式平均情形复杂度分析。
HoCHC：一个反驳完备且语义不变的高阶逻辑模理论系统
为高阶约束 Horn 子句提出简单归结证明系统，并证明其在标准与 Henkin 语义下可靠且反驳完备。
视角博弈（Perspective Games）
提出视角博弈模型，其中玩家仅观察自己拥有的顶点，并研究其获胜策略判定、ATL*模型检测及策略表达能力。
概率高阶递归程序的终止问题
提出 PHORS 概率高阶程序模型，证明二阶几乎必然终止不可判定，并给出终止概率的不动点刻画与近似算法。
λ演算与概率计算
为λ演算引入概率选择算子，建立按值/按名语义下的合流与标准化理论。
匹配 μ-逻辑
为匹配逻辑给出可靠完备证明系统，并扩展出匹配 μ-逻辑，统一刻画多种不动点、模态与时序逻辑。
通过延迟迹的可微因果计算
用范畴论中的延迟迹统一建模因果计算，并给出无需展开的状态网络反向传播微分算子。
酉球中的可实现性
提出基于可实现性的线性代数 λ-演算语义，刻画酉性并导出类型规则，可扩展至经典与量子 λ-演算。
反向传播作为函子：监督学习的组合视角
将反向传播范畴化：证明梯度下降是从参数化函数到更新规则范畴的 monoidal functor，并引入 request function。
有限可生成子集的凸包及其谓词变换器
用域论构造有限可生成子集的可计算凸包映射，并导出其谓词变换器。
固定维数下向量加法系统的可达性是原始递归的
通过改进经典分解算法及其终止性证明，将固定维数 VAS 可达性上界降至原始递归，并给出一般情形的 ACKERMANN 上界。
面向纯量子比特量子力学的 ZX-Calculus 近极小公理化
提出两种 ZX-Calculus 完备公理化，规则近乎极小且具物理直观，并引入 ZX 图奇异值分解证明其充分性。
超逻辑的层级结构
系统比较超逻辑的两类扩展，给出表达能力层级，并界定可满足性可判定边界。
带幽灵变量的量子 Hoare 逻辑
提出带幽灵变量的量子 Hoare 逻辑扩展，增强前后条件表达能力，并验证量子一次性密码本安全性。
面向互模拟的 Codensity 博弈
提出基于纤维化与余代数的统一范畴框架，将互模拟类概念的博弈刻画导出为 Codensity 互模拟博弈。
近似 span 提升：差分隐私松弛的组合语义
提出近似 span 提升，为多种差分隐私松弛提供组合语义与可证明其性质的程序逻辑。
分配律的 No-Go 定理
提出两类 No-Go 定理，判定两个 monad 间不存在 Beck 分配律，统一并扩展已有结果。
非确定性与概率系统的迹理论
用余代数广义幂集构造统一导出并比较非确定性与概率系统的迹等价语义。
带星号的 Presburger 算术、图群的有理子集与嵌套零测试
证明带星号的存在性 Presburger 算术为 NEXP 完全，并统一三个判定问题及其固定参数复杂度。
逻辑视角下的时间系统
用EQ-ICPDL刻画带严格时间约束的图可实现性，为带栈/队列等数据结构的时间系统提供统一高效验证技术。
一阶文法的互模拟等价性是 ACKERMANN-完全的
首次给出下推自动机弱互模拟等价判定的 ACKERMANN 复杂度上界，并证明其最优。
带优先级的 Lambda Y 演算
将高阶模型检测归约为带优先级 Lambda Y 演算与可见奇偶自动机，并证明幂集模型是正确语义框架。
结合 n-范畴中同伦构造的高层方法
提出 contraction 操作，在结合 n-范畴中算法化构造复杂同伦，并在 homotopy.io 证明助手中实现。
路径性质的长期满足性
引入 Kripke 结构与 MDP 中路径性质的长期频率/概率，并刻画其最优值与阈值判定问题的复杂度。
表示条件独立性的算法障碍
证明可计算采样的可交换随机图其 graphon 表示不可计算，揭示条件独立性表示存在算法障碍。
MSO+∇ 是不可判定的
证明带几乎必然分支量词的 MSO+∇ 在完整二叉树上真值判定不可判定。
描述自由 ω-范畴
用 Agda 证明 parity complexes 不满足自由性，并提出满足自由性的修正形式化。
时间旅行的范畴语义
提出弱化迹幺半范畴的范畴框架，为含闭合类时曲线的量子过程理论提供统一语义。
LICS 1999 Test-of-Time Award 颁奖引文
2019年LICS Test-of-Time Award表彰1999年两篇关于带绑定变量抽象语法的开创性论文。
一个概率与非确定性的 Call-by-Push-Value 语言
提出概率与非确定性 CBPV 语言，用两类类型绕开连续 domain 语义障碍，并证明可靠、充分与完全抽象。
定义逻辑与证明的类型理论
提出依赖类型理论 Cocon，融合 HOAS 与可计算函数空间，并用 Kripke 模型证明规范化与一致性。
历史依赖的 nominal μ-演算
通过引入对全局历史中原子的新鲜性测试，扩展 nominal μ-演算，并证明其模型检测可判定。
图形仿射代数
通过仿射连接子扩展图形线性代数，给出图形仿射代数在自然数模与域上模两类语义下的完备公理化。
有界秩宽图的典范化与可定义性
证明(3k+4)维Weisfeiler-Leman算法完全判定秩宽≤k图的同构，并得到多项式时间典范化与计数固定点逻辑刻画。
模拟与量子资源的余单子视角
提出余单子与 co-Kleisli 范畴刻画经验模型间模拟，统一量子资源理论中的自由操作。
高阶 Kind 数据类型：语法与语义
提出统一语法与范畴语义，证明含 GADT 与高阶 Kind 的数据类型在局部可表现范畴中具有函子式初始代数语义。
模板博弈与微分线性逻辑
首次为经典形式的微分线性逻辑建立博弈语义，并揭示其与同伦论的意外联系。
博弈逻辑的完备性
通过无割矢列演算与到单调 μ-演算的翻译，证明 Parikh 博弈逻辑及其 Hilbert 公理系统的完备性。
面向笛卡尔闭双范畴的类型理论（扩展摘要）
为笛卡尔闭双范畴构造内部类型理论，将 Curry-Howard-Lambek 对应提升到双范畴情形。
动作格的逻辑不可判定
证明剩余 Kleene 格（动作格）的（不）等式理论不可判定，解决了长期开放问题。
量子信道作为范畴完备化
用分配单体范畴证明量子信道范畴是纯量子操作范畴的典范完备化，并推广至拓扑丰富情形。
论 Büchi 算术与线性 p-adic 域的存在理论
证明 Büchi 算术与线性 p-adic 域存在片段的可满足性问题均为 NP 完全。
无语法表示的直觉主义证明
提出直觉主义组合证明（ICPs），一种复杂度感知的几何语义，多项式保持序列演算翻译并实现局部典范性。
本体介导查询何时是高效的？
刻画基于描述逻辑的本体介导查询何时可处理或固定参数可处理，并研究其有界树宽等价性判定问题的复杂度。
为什么命题量化使树上的模态逻辑具有鲁棒难解性？
证明树上命题量化模态逻辑的 EX 片段已 Tower-hard，并给出有界树上的 AExppol-完全性。
拓扑是相关的（无限域约束满足问题的二分猜想中）
证明无限域 CSP 二分猜想中高度 1 恒等式的局部与全局满足不同，拓扑不可忽略。
点宽度与 Max-CSP
提出超图点分解框架，给出统一 β-无环性与有界 MIM-width 的 Max-CSP 易解性条件。
承诺使有限（约束满足）问题无穷化
证明 (1-in-3-SAT, Not-All-Equal-3-SAT) 不能自然归约到可解有限域 CSP，除非 P=NP。
Opetopes 的矢列演算
为 opetopes 与 opetopic 集提出纯语法的矢列演算，并证明良类型 opetope 与传统定义一一对应。
期望有限时域下的图规划
证明对抗性停止时间分布下图规划的最优平稳计划存在，并给出多项式时间算法。
可数词上代数的块积及其在逻辑中的应用
将块积运算融入可数词正则语言的代数框架，并用迭代块积刻画一阶逻辑与线性时序逻辑片段。
约束满足问题（CSP）二分猜想简史
回顾约束满足问题（CSP）复杂度二分猜想的提出背景，说明为何要在广泛问题类上研究 P/NP 二分现象。
Horn 描述逻辑的模型比较博弈
为 Horn 描述逻辑 hornALC 引入模型比较博弈，给出可定义性与表达完全性结果，并证明其不可区分性检查为 ExpTime 完全。
学习带计数一阶逻辑中可定义的概念
证明多对数度结构上 FOCN(P) 可定义概念可亚线性学习，而无界度下即使一阶公式也不存在亚线性学习算法。
同伦类型论中高阶归纳类型的路径空间
证明高阶归纳类型等式类型的通用路径空间定理，并在 Lean 中形式化。
游走精化、游走逻辑与 Weisfeiler-Leman 算法的迭代次数
证明 2-维 Weisfeiler-Leman 算法至多 O(n log n) 次迭代稳定，并引入游走精化与游走逻辑给出匹配线性界。
基于群的拼接层级的分离与覆盖
对基类只含群语言的拼接层级，证明若基类分离可判定，则低层（1/2、1、3/2）分离与覆盖均可判定。
论对称线性规划的能力
证明对称线性规划族与对称阈值门布尔电路等价，并给出非一致FPC刻画及匹配与哈密顿图的上下界。
ZX-图的一般范式及其在有理角完备性中的应用
为 ZX-图给出通用范式与算法，并证明 Clifford+T 公理对二进角及有理角片段的完备性。
局部范式及其在算法元定理中的应用（特邀报告）
从个人视角综述局部范式及其在算法元定理中的近期应用进展的特邀报告。
元胞自动机最小时间的描述复杂度
用存在二阶 Horn 逻辑刻画一维元胞自动机实时（最小时间）复杂类，并给出网格电路归一化方法。
LICS 2019 前言
简要介绍第34届 ACM/IEEE 计算机科学逻辑研讨会（LICS 2019）的会议与论文集信息。
201891 篇 · Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
持续推理
提出持续推理，将形式化推理融入持续迭代的代码库开发，以扩展形式化方法的适用范围。
计算图抽象的几何
用动态交互几何为按值λ演算中的计算图抽象建立类型系统与语义模型，保证垃圾回收和β律安全。
ReLoC：一种用于高阶状态、细粒度并发、多态与递归类型程序精化的逻辑
提出 ReLoC，一种用类型与结构导向规则证明高阶状态、细粒度并发、多态和递归类型程序精化的逻辑。
用于时序性质验证的不动点逻辑与依赖效应
提出依赖精化类型与效应系统及不动点逻辑演绎方法，以组合化验证高阶函数式程序的时序性质。
从模态 μ 演算视角求解奇偶博弈的准多项式时间算法
提出基于 register-index 的奇偶博弈新准多项式求解算法，固定参数下多项式可解。
随机 λ-演算的布尔值语义
提出随机 λ-演算的布尔值语义，用测度代数解释高阶概率程序并支持等式推理。
马尔可夫决策过程中基于分布的目标
研究 MDP 中基于分布的目标如何在完全信息与部分信息之间取得策略层面的权衡。
实数及其他空间上的可计算决策
提出基于构造拓扑的程序语义，利用非确定性/部分性及空间模式匹配，在精确实数计算中实现可计算的离散决策。
黑暗中的黑忍者
以交互式论文形式介绍种群协议这一分布式计算基础模型，并综述作者近期关于其自动验证的工作。
资源感知会话类型的工作量分析
提出资源感知会话类型，静态推导消息传递并发进程的最坏情况总工作量。
仿射程序的多项式不变量
提出计算仿射程序各位置最强多项式（代数）不变量的算法，核心是计算有理矩阵生成半群的 Zariski 闭包。
健全的 up-to 技术与完备抽象域
研究 sound up-to 技术与完备抽象域之间的关系，连接余归纳与抽象解释。
定量类型理论的语法与语义
提出定量类型理论，并给出基于线性组合代数与定量CwF的资源敏感实现性语义。
纯态量子比特量子计算的两个完备公理化
为纯态量子比特量子计算的 ZW 与 ZX 图示演算给出两个完备公理化。
高阶效应程序的定量行为推理
为带代数效应的高阶 λ-演算建立 quantale 值行为相似与双相似，并证明其分别为相容的广义度量与伪度量。
概率PCF的并发博弈语义
提出概率PCF的并发博弈语义，证明其内涵完全抽象并给出有限可定义性。
一个定理统御一切
提出一个统一主定理，将 LTL 公式翻译为确定性 Rabin、极限确定 Büchi 和非确定 Büchi 自动机，均达渐近最优规模。
微分方程公理化
证明微分动态逻辑的微分方程公理对所有代数不变式完备，并用微分幽灵构造证明。
带作用域操作的语法与语义
提出带作用域操作的抽象语法的范畴模型，以分离代数效应与处理器的语法和语义。
关联度
提出用模态标注函数类型，在依赖类型论中为关系参数性提供类型级保证，从而安全省略证明。
一种面向混合动态信息流的混合动态逻辑
提出首个验证信息物理系统中混合动态信息流安全性的逻辑 dHL，并给出可靠证明演算与电网案例。
一种用于递归的广义模态
提出递归的广义模态，将 Nakano 的 later modality 推广到更一般的范畴框架。
离散锥上的概率稳定函数是幂级数
证明离散锥上的概率稳定函数可视为广义幂级数，并将概率相干空间嵌入连续概率模型 Cstabm。
不完全信息下的理性合成
研究不完全信息下多玩家非零和游戏的理性合成，证明二人奇偶目标为 ExpTime 完全，三人以上不可判定。
（高阶）归纳类型的非直谓编码
提出用同伦类型论思想精化非直谓编码，使有限归纳类型恢复 η 等式与依赖消去，并扩展到部分高阶归纳类型。
一种简单且最优的 Büchi 自动机求补算法
提出一种直接在状态子集上运行、结构简单的确定性 Büchi 自动机求补算法，并证明其达到最优上界。
由 SMCC 加权的 species、profunctor 与 Taylor 展开
引入以 SMCC 加权的广义 species/profunctor，证明其构成 Lafont 范畴，并统一线性逻辑与多类编程语言的定量模型。
树上的 MSO 查询
本文给出树上的 MSO 查询在局部更新下的高效枚举算法，预处理 O(n)，答案延迟 O(log n)，更新后 O(log n) 恢复。
马尔可夫过程的代数理论
用定量等式逻辑与单子组合，给出离散/连续状态空间马尔可夫过程的代数公理化。
寄存器监控器理论
提出带整数寄存器的无限状态监控器模型，并刻画其按寄存器数量与指令类型的表达能力层级。
稀疏结构上模型检测的参数化电路复杂度
证明有界扩张图类上的一阶模型检测可由参数化 AC 电路判定，属于 para-AC^1。
mean-payoff parity 博弈的伪拟多项式算法
为 mean-payoff parity 博弈提出一种伪拟多项式时间求解算法。
通过选择序列超越 Church-Turing 可计算性
提出扩展 Nuprl 类型论的新类型论 BITT，用 Beth 式语义嵌入自由选择序列并验证其关键公理。
一种带状态的函数解释
提出带全局状态的 Gödel 函数解释，用状态有效性处理 contraction，并改进证明抽取程序的效率与语义理解。
Clifford+T 量子力学的 ZX-Calculus 完全公理化
为 Clifford+T 量子力学提出首个完全且近似通用的 ZX-Calculus 公理化，并证明其 π/4 片段完备。
多值电路的可满足性
将布尔电路可满足性推广到任意有限域上的多值电路，并揭示其复杂度与有限代数方程求解的紧密联系。
带状张量逻辑
提出带状张量逻辑，将证明映射为带状缠结并证明该翻译忠实，从而给出平衡对话范畴的相干定理与拓扑博弈语义基础。
概率Böhm树与概率分离
定义概率Böhm树与Nakajima树，推广Böhm-out技术以分离概率分布，推进概率λ演算的分离定理。
并发与概率
用结构分支单元（s-cell）把 Petri 网静态分解并转换为无混淆网，从而统一刻画并发与概率选择。
带依赖类型的经典算术相继式演算
提出带依赖类型的经典算术相继式演算，以攻克 dPAω 中依赖类型、控制算子、余归纳与惰性共享共存下的正规化难题。
超越二变量逻辑的加权模型计数
将FO2上WFOMC的多项式时间结果扩展到唯一存在量词扩展与U1片段，并给出前缀类复杂度完全分类。
分布式进程的因果计算复杂度
为 π-演算进程结合多项式终止类型与因果语义，建立外部消息因果触发的多项式消息复杂度界。
正则与一阶列表函数
定义正则/一阶列表函数，并证明它们分别恰好对应 MSO 转换与一阶转换。
并发分离逻辑的异步可靠性定理
用异步博弈语义为并发分离逻辑建立异步可靠性定理，并解释其常规可靠性及无数据竞争。
LMSO：通过线性逻辑的 Curry-Howard 方法进行 Church 合成
提出 LMSO 证明系统，从 ω-正则规范的线性构造性证明中提取有限状态流转换器。
可组合博弈论
提出开放博弈，以对称幺半范畴与弦图给出博弈论的可组合基础，并保持纳什均衡。
围绕经典线性逻辑与直觉主义线性逻辑
在命题情形下重新审视并梳理经典线性逻辑与直觉主义线性逻辑各变体之间的句法关系。
词转换及其合成的逻辑
提出逻辑 ℒT，用 origin 函数刻画词转换的输入输出依赖，可表达所有正则函数式转换（如确定性双向传感器）。
CTL 成员性的自动机基准则
提出基于自动机的 CTL 成员判定准则，为判断 LTL 公式是否可由 CTL 定义提供条件。
马尔可夫决策过程中面向可达性与平均收益的条件风险价值（CVaR）
研究MDP中可达与平均收益目标下CVaR及其与期望、VaR约束组合的决策复杂度与策略结构。
经典可实现性作为非确定性的分类器
用经典可实现性模型刻画非确定性程度，并证明可实现性模型的布尔代数与底层计算模型非确定性程度之间的对偶。
同伦类型论中的高阶群
在同伦类型论中发展高阶群与连接谱理论，并证明稳定化定理，多数结果在 Lean 中形式化。
可定义椭球法、平方和证明与同构问题
证明椭球法可在带计数不动点逻辑 FPC 中定义，在无穷 FPC 中表达 SDP 精确可行性，并推出图同构的 SoS 层级塌缩到 Sherali-Adams 层级。
超越 Clifford+T 量子力学的图解推理
证明 Clifford+T 的 ZX 演算公理对线性图完备，并只需增加一条非线性公理即可完备于纯 qubit 量子力学。
马尔可夫决策过程中的随机最短路径与权重有界性质
提出端分量分类算法，求解整数权重 MDP 的随机最短路径与权重有界可达性问题并给出复杂度界。
聚焦逻辑中的强和（strong sums）
将强和（strong sum）引入聚焦逻辑，并指出其右投影类型依赖被投影项所带来的适配难题。
分配森林代数的圈积
证明满足二重迭代分配律的森林代数所识别语言均属于 PDL，并给出该子类的可判定性。
带等价关系的一元否定片段具有有限模型性质
证明带任意多等价关系的一元否定片段具有有限模型性质，并确定其可满足性为 2-ExpTime 完全。
VASS 中终止时间渐近界的高效算法
为 VASS 终止时间的渐近复杂度提供多项式时间判定与分类，并给出最优多项式次数计算。
关系参数性的一个通用框架
提出了一个能忠实表达 Reynolds 原始关系参数性理论的一般框架。
单价性的内模型
为依赖类型论给出一类保持单价性（univalence）的简单内模型构造。
线性类型化作为三价图上的流：一种理论
将线性 lambda 项的类型化解释为嵌入三价图上的流，并刻画局部流关系可提升为全局流关系的条件。
用于正则变换的正则变换器表达式
证明确定性双向变换器定义的有限/无限字正则函数均可由正则变换器表达式（RTE）描述。
论稀疏图中类型的数量
证明 nowhere dense 图类中一阶可定义集合系统的 VC 密度上界为 O(|A|^{|x|ε})，并给出准宽与稳定性的构造性新证。
富化一个线性/非线性 lambda 演算
为线性/非线性 lambda 演算的 string diagram 语言建立富化语义模型，并扩展一般递归与证明可靠性/充分性。
带 mismatch 的准开放互模拟是直觉主义的
将准开放互模拟扩展到含 mismatch 的 π-演算，证明其与开放 barbed 互模拟一致，并有直觉主义模态逻辑刻画。
分段可测语言的可分离性与超越子词序的向下闭包
引入泛化子词序的良拟序，将分段可测语言可分离性与向下闭包计算归约到同时无界问题，并证明一阶片段 BΣ1[<, mod] 的可分离性可判定。
类型论的 Dialectica 模型
基于 Gödel 的 Dialectica 解释及其 Diller–Nahm 变体，为内涵 Martin-Löf 类型论构造两种范畴模型。
合一证明网
提出消除存在量词见证冗余的 MLL1 规范证明网——合一证明网。
急切函数作为进程
证明按值调用 λ-演算编码进两个 π-演算子演算后，所诱导的项等价恰为含 η-等式的 Lassen 急切范式互模拟。
二型多项式时间与受限前瞻
通过限制预言机查询的前瞻修正次数，给出无需高阶运行时间的二型多项式时间可计算性新刻画。
线性偏微分方程的逻辑解释
构造 DiLL 的经典指称语义模型，基于核拓扑向量空间与紧支分布，使证明的线性近似对应通常微分。
带阈值算子的 Riesz 模态逻辑
为带阈值算子的 Riesz 模态逻辑给出可靠完备公理化，使其能刻画离散与连续 Markov 链上的概率 CTL 有界片段。
树深度、量词消去与量词秩
研究图类上有界树深度、FO 有效广义量词消去与参数化模型检测复杂度之间的等价关系。
守卫计算类型论
提出守卫计算类型论，将 Nakano later 模态、时钟变量与依赖类型及宇宙层级相结合。
小深度布尔与算术电路类的模型论刻画
利用带归纳关系算子和语义博弈计数的新逻辑，统一刻画对数深度布尔与算术电路类。
博弈中有什么？
提出统一的博弈语义抽象框架 game settings，并泛型构造博弈与策略范畴，统一早期与层论模型。
用 Frobenius 重写
在对称幺半范畴的 string diagram 推理中，结合 Frobenius 与 DPO 超图重写，吸收结构定律并仅显式保留领域方程。
论无限集合的可计算性与易处理性
提出可定义 while 程序，刻画遗传可定义集合上的可计算函数，并定义固定维多项式时间复杂性类。
Allegories
证明 allegory 的等式理论可判定，并用一类图同态给出刻画。
参数化停机问题、线性时间层级与 MRDP 定理
将参数化停机问题 p-Halt 是否属于 para-AC0 与经典复杂性开放问题 NE ⊈ LINH 相联系，表明其难以判定。
同伦类型论中的自由高阶群
在同伦类型论中研究自由高阶群 F(A) 何时为集合，证明其基本群平凡，即 ||F(A)||₁ 是集合。
交替自动机的状态复杂度
研究无限交替自动机的状态复杂度，将 Karp 状态复杂度框架拓展至超越正则语言的语言类。
能否逃离 Red Chains？
研究查询决定性：给定查询集合与目标查询，判断视图信息是否足以计算目标查询结果。
外延与内涵语义宇宙
提出一种同时包含内涵与外延语义宇宙的依赖类型理论及其指称模型，其中项与类型分别解释为图博弈策略和事件域上的稳定函数。
模糊模态逻辑的 van Benthem 定理
证明了模糊一阶逻辑中相对于双模拟距离非扩张的公式恰可由模糊模态公式逼近。
论立方类型论中的高阶归纳类型
为立方类型论中的若干高阶归纳类型给出构造性语义与语法扩展，并证明判断性计算规则和宇宙封闭性。
量子计算中的逻辑悖论
从逻辑悖论角度讨论量子计算中语境性、magic states 与量子计算能力来源之间的联系。
无穷关系模型中每个 λ 项都有意义
证明在无穷关系模型中每个 λ 项都有非空指称，并用无穷交类型刻画其元数。
单调单子 SNP 复杂性二分性的通用代数证明
为 MMSNP 到有限域 CSP 的归约给出新证明，并验证其复杂性二分猜想。
Gamma 问题的一个解答
回答了粗可计算性中的 Gamma 公开问题，澄清 oracle 集合的 Gamma 值能否严格介于 0 与 1/2 之间。
201796 篇 · 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
面向高阶概率论的一个方便范畴
提出准博雷尔空间，为高阶概率程序提供兼具连续分布与高阶函数的范畴语义。
混合符号期望的最弱前置期望语义
提出可处理混合符号无界随机变量期望的概率程序最弱前置期望演算，保证语义总良定义且可靠。
符号执行与概率推理
将符号执行与概率推理结合，通过模型计数计算程序目标事件的发生概率，用于软件安全与可靠性分析。
基于余递归代数的范畴活性检查
用余递归代数与余代数模拟，统一范畴化活性验证中的 ranking function 与 ranking supermartingale。
若干无限状态 MDP 与随机博弈的算法
综述无限状态 Markov 链、MDP 与随机博弈的算法与复杂度，统一递归/计数器式概率程序模型。
不完美信息下的策略逻辑
提出不完美信息策略逻辑SLii，识别可判定的分层片段并归约至QCTLii*加以证明。
求解奇偶博弈的简洁进度测度
提出基于进度测度的准多项式时间奇偶博弈求解算法，将空间需求从准多项式降至近线性。
有限模型论中的 pebbling comonad（卵石余单子）
为存在式 k-卵石游戏引入余单子，用 coKleisli 态射统一刻画有限模型论多个核心概念。
子词序上一阶逻辑的可判定性、复杂性与表达力
确定子词序上一阶逻辑的可判定边界，并证明所有变量交替受限时整一阶理论可判定。
无限域约束满足问题的两个二分猜想的等价性
证明无限域 CSP 的两个二分猜想等价，并用轨道增长、Ramsey 性质与线性恒等式给出新结果。
算术下归纳定义与循环证明的等价性
证明在加入算术后，循环证明系统 CLKID-omega 与 Martin-Löf 归纳定义系统 LKID 的证明能力等价。
时钟在滴答：不再有延迟！
提出 Clocked Type Theory，为守卫递归给出适合归约语义的类型论，并证明合流、强规范化与典范性。
一种消除依赖成瘾的效应化方法
提出 weaning 翻译，首次在依赖类型论 CIC 中安全引入异常、非终止、非确定性等计算效应。
λ演算的定量语义：关系模型的一些推广
综述λ演算的定量语义，证明关系语义、HO/N博弈语义与Taylor展开语义等价，并讨论两类关系模型推广。
线性时间 μ-演算的构造性完备性
为线性时间 μ-演算的 Kozen 公理化给出构造性完备性证明，对每个有效公式构造证明。
在小度数结构上学习一阶可定义概念
证明在度数至多多对数的背景结构上，一阶公式定义的概念可在多对数时间内PAC学习。
Petri 网和带状态向量加法系统中连续可达性的逻辑
刻画连续 Petri 网与 CVASS 的可达集，证明 CVASS 可达性 NP 完全，并给出若干多项式时间判定算法。
可数 MDP 中的奇偶目标
研究可数无限 MDP 的奇偶目标及其 Mostowski 层级中有界颜色特例（可达、安全、Büchi、co-Büchi）。
面向完全基类型引用单元的 monad
用函子范畴上的 monad 给出可含环引用单元的指称语义，并支持效应屏蔽与代码变换验证。
高阶奇偶自动机
提出高阶奇偶自动机，将奇偶树自动机推广到无穷简单类型 λ-项，并证明由 λY-项生成的项接受性可判定。
完美半空间博弈
引入完美半空间博弈并证明其位置确定性，进而以伪多项式时间求解多维能量奇偶博弈。
高阶逻辑中基础性的非均匀（余）数据类型
将一大类非均匀（嵌套）数据类型与余数据类型归约到高阶逻辑中的均匀类型，并在 Isabelle/HOL 中实现。
同伦类型论中的实射影空间
在同伦类型论中用高阶归纳类型与 tautological bundle 归纳构造实射影空间。
作为序列的无穷交类型：Klop 问题的新答案
提出 System S，用序列化无穷交类型刻画弱规范化项，正面回答 Klop 问题。
关于 max-plus 自动机的延迟与遗憾确定化
提出 k-delay 与 r-regret 确定化，证明其 EXPTIME 完全性并刻画与一般确定化的关系。
模态逻辑的双上下文演算
为 K、T、K4、GL、S4 的必要性片段提出双上下文自然演绎与模态 λ 演算，并建立元理论与范畴语义。
带线性算术的寄存器自动机
提出有理数上的寄存器自动机 RA_Q，支持线性算术，并证明其不变量问题可判定。
带能量-奇偶目标的 MDP
研究奖励 MDP 中控制器如何在避免能量耗尽的同时满足奇偶目标。
重新审视时间自动机中的可达性
给出时间自动机二元可达关系可在线性算术中定义的新简化证明，并用于参数化 TCTL 可达片段的模型检测与复杂度下界。
用于高阶模型检测的笛卡尔闭范畴
为高阶模型检测构造笛卡尔闭范畴，并借助Büchi自动机的有限抽象格实现忠实抽象与不动点计算。
线性方程组的描述复杂度及其对命题证明复杂度的应用
证明线性方程可解性可在仅多对数次迭代的带计数不动点逻辑片段中定义，并据此分离若干逻辑与证明系统。
Bar induction：好、坏与丑
为 Nuprl 扩展 bar induction，在 Coq 中证明其可靠性与一致性，并发现单调 bar 的非截断版本直觉主义下不成立。
时间下推自动机与分支向量加法系统
证明定时寄存器下推自动机的非空性可判定，并给出两个相关系统的指数时间判定结果。
随机化安全协议的验证
证明随机化安全协议的保密性与不可区分性可在 coNEXPTIME 内判定，并给出保密性匹配下界。
马尔可夫过程的非受限 Stone 对偶
为马尔可夫过程建立无受限 Stone 型对偶，扩展 Sikorski 可测空间对偶并清晰刻画事件互模拟。
有界扩张图类上后继不变一阶公式的模型检测
证明有界扩张图类上后继不变一阶公式的模型检测问题是固定参数可处理的，推广了先前结果。
在初等时间内解缠双向转换器
提出双指数空间算法判定双向转换器实现的函数是否可由单向转换器实现，并扩展至扫掠转换器。
纤维化的纤维化范畴
引入纤维化的类型论纤维化范畴，为恒等类型的逻辑谓词提供范畴语义，并导出同伦类型论的关系参数性。
单计数器自动机的正则可分离性
证明了无零测试单计数器自动机语言的正则可分离性可判定且为 PSPACE 完全。
计数查询答案的逻辑
提出并研究一种扩展一阶逻辑，用其自然表达有限结构上一阶公式答案计数的算法，以刻画易解情形。
计算具有多维成本的马尔可夫链中的分位数
提出任意精度近似多维成本马尔可夫链总成本分位数的算法，并证明其判定版本属于计数层级。
Markov 过程的 Riesz 模态逻辑
提出以 Riesz 空间对偶为语义的实值模态逻辑，并给出 Markov 过程的可靠完备公理化。
闭空间中的枚举归约性及其在逻辑与代数中的应用
在闭空间中引入枚举归约性，用以统一解释逻辑与可计算代数中不可判定问题在加入刚性条件后可判的现象。
确定性协商的静态分析
证明确定性协商图（等价于自由选择工作流 Petri 网）的健全性、摘要与期望成本等静态分析问题可在 PTIME 内求解。
逻辑与正则代价函数
综述正则代价函数理论，并阐述其与逻辑及正则语言理论的两条联系。
带代价与延迟的博弈
研究带代价的延迟无限博弈，证明其获胜判定为 EXPTIME 完全，并刻画延迟与策略质量间的权衡。
行列式恒等式的统一、整数与高效证明
在 VNC2 中证明整数上行列式乘法性，给出统一的 O(log²n)-深度多项式规模 Circuit-Frege 证明及 NC2 代数电路算法。
逻辑形式中的微分
用邻近格上的可逼近映射与 Stone 对偶，为局部 Lipschitz 映射的 Clarke 次梯度建立逻辑形式的微分理论。
模态 μ-演算的无割完备性
为模态 μ-演算给出两个有限无割矢列演算，并由此构造性地证明 Kozen 公理系统的完备性。
带效应的应用性互模拟：单子、relator 与 Howe 方法
在带代数效应的 call-by-value λ-演算中，用 monad 和 relator 抽象推广应用性互模拟，并刻画其成为同余的条件。
论定量代数的可公理化性
系统刻画定量代数可由简单定量等式、受限及一般 Horn 子句公理化的范围，并证明相应簇/拟簇定理。
带计数的一阶逻辑
提出 FOCN(ℙ)，用计数与数值谓词统一泛化多种已有计数逻辑。
多项式自动机：零性问题与应用
引入多项式自动机，刻画其零性问题的复杂度，并应用于 VAS 覆盖性与流式字符串转换器等价性。
刚性资源项的广义 species
引入刚性资源演算，使 Taylor 展开与广义 species 解释一致，并证明 Böhm 树与 Taylor 展开交换。
类型论的栈语义
用栈模型解释带一个泛等宇宙与命题截断的依赖类型论，并证明可数选择不可证。
bag 语义下信息集成的基础
为数据交换与信息集成建立 bag（多重集）语义基础，并揭示其导致计算复杂性的上升。
弱 ω-范畴的类型论定义
提出一种依赖类型论，其模型恰为弱 ω-范畴，并给出粘贴方案的类型论刻画与证明系统实现。
拟严格高阶范畴的数据结构
提出拟严格高阶范畴的数据结构，支持4-范畴计算并机器验证了一类伴随提升定理。
Gödel 逻辑：从自然演绎到并行计算
为命题 Gödel 逻辑 G 建立 Curry–Howard 对应，用自然演绎类型系统刻画带同步通信的并行函数式计算。
使用知识编译理解 #SAT 的复杂度
通过电路表示分离 #SAT 的两类求解技术，揭示 β-acyclic 公式的复杂度。
Kleene allegories 的图上偏导数
证明 Kleene allegories 等式理论可判定且为 EXPSPACE 完全，并用图上偏导数给出自动机构造。
半定规划的可定义性与CSP的Lasserre下界
证明椭球法可在带计数的不动点逻辑中表达，并由此导出VCSP的Lasserre层级下界。
并发交互的几何：以多令牌方式处理多端口
为Mazza多端口交互组合子提出多令牌几何交互模型，并证明其可靠性与充分性。
有界维度下的可类型性
证明有界维度交集类型的可类型性在集合论与多重集模型下均可判定，并给出 PSPACE 完全与 NP 复杂度。
递归的 lean 与 full 同余格式
区分递归的精简与完全同余，证明 bisimilarity 在 ntyft/ntyxt 下满足 lean 同余，在 tyft/tyxt 下满足 full 同余。
一系列高效模拟算法的基础
提出极大迁移与预序稳定性，为一系列高效模拟算法奠基，并给出首个兼顾时间与空间复杂度的最粗模拟预序算法。
分离片段中困难问题的细粒度层级
通过引入存在变量交互度，证明分离片段可满足性在有界度数下恰为 k-NEXPTIME 完全，并推出一般情形非初等。
无序数据向量的线性组合
研究可数域上数据向量能否由有限基向量的置换等价类通过有限和表示。
半格块 Mal'tsev 代数上的约束满足问题
提出结合局部传播与解空间基的混合方法，证明半格块 Mal'tsev 代数上的 CSP 多项式时间可解。
正则图模式的同态问题
系统研究正则图模式同态问题，揭示其复杂度高于同态问题并给出二分猜想与保证高效的结构限制。
语言上的量词与余密度单子
通过余密度单子与对偶理论，在识别器上添加量词层，证明 Reutenauer 型定理并刻画 profinite 单子。
dot-depth 2 的分离
本文给出 dot-depth 2 的分离算法，并证明基类有限时该层级第 1 层分离可判定。
面向融合的域与事件结构
提出 connected event structures 及其对偶域，刻画非线性图重写等融合计算的并发语义。
度量空间与 Banach 空间上的有界时间计算
将二阶复杂度理论经表示提升到度量空间与 Banach 空间，扩展分析中算子的有界时间计算框架。
平面图的 Weisfeiler-Leman 维数至多为 3
证明所有有限平面图的 Weisfeiler-Leman 维数至多为 3，将此前上界从 14 改进到 3。
可数随机博弈的强确定性
研究可数无穷状态随机博弈在可达、Büchi、ω-正则等目标下的强确定性。
Herbrand 性质、有限准 Herbrand 模型与量化合取查询的 Chandra-Merlin 定理
提出 Herbrand 性质与有限准 Herbrand 模型，判定量化合取查询包含问题并给出紧复杂度界。
一般值 CSP 的 SDP 松弛的极限
论文研究一般值 CSP 的 SDP 松弛能力极限，并联系 Sherali-Adams LP 层次与 bounded width 条件。
阿贝尔群与半群求和问题的可定义性
证明阿贝尔群/半群求和问题在带计数固定点逻辑 FPC 中可定义，且计数算子不可去除。
通过 bar recursion 解释 System F
首次将 System F 翻译到带 bar recursion 的简单类型全语言，并基于可实现性给出归一化解释。
Cayley 结构中的公共知识与多尺度局部性分析
用 Cayley 群表示认知框架，给出带公共知识的多主体模态逻辑的 van Benthem 式刻画与多尺度局部性分析。
包含式合取下二元关系代数中算子的本原性
研究二元关系代数在包含式合取下的算子本原性，证明除有限互依外每个特性都本原。
无限字符串的大尺度几何
将大尺度几何引入形式语言，用拟等距刻画无限字符串全局模式，并研究与 Büchi 自动机和可计算性的联系。
单子流函数的连续性
研究 Brouwer 连续性原则下单子流函数的连续性及其在类型论中的不一致性边界。
单子编程中的商：投射代数等价于余代数
证明单子编程中投射代数范畴等价于单子分解所诱导余代数的范畴，从而可用余代数实现多态商类型。
论平移不变极大滤子与激素元胞自动机
构造 ℤ 上平移不变极大滤子，用以定义并分析带全局信息的激素元胞自动机模型。
使用模块分解捕获多项式时间
提出模块分解定理，将图类可定义规范化归约到素图，证明带计数不动点逻辑在排列图上捕获多项式时间。
Crane Beach 上的一道裂缝：有限度谓词
证明 FO[A_RB] 与 FO[≤, MSB0, F_IN] 等表达，且 FO[≤, F_IN] 和 FO[≤, MSB0] 满足强 Crane Beach 性质。
论可计算实函数的延拓
研究定义在左可计算实数边界区间上的可计算实函数何时能可计算延拓，并刻画其充要条件。
通过抽象机实现 λ-演算到 HOcore 的完全抽象编码
通过抽象机证明 call-by-name λ-演算到 HOcore 的完全抽象编码，并统一多种等价关系。
LICS 2017 前言
介绍 LICS 2017 会议论文集、会议信息及七个同期研讨会，不包含具体研究贡献。
保守约束语言下最小推理问题的复杂度
对保守约束语言上的命题限定最小推理问题给出复杂度三分法：Π₂ᵖ-完全、coNP-完全或 P。
LICS 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2017
LICS 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2017
LICS 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2017
LICS 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2017