一句话：完整描述并实现支持宇宙多态与重载（规范结构）的 CIC 合一算法，并在大型库上验证启发式足够。
论文关注带依赖类型的证明助手与编程语言中的合一问题。CIC（Coq 的基础逻辑）需要处理转换下的高阶合一，该问题不可判定，现有合一器依赖多种启发式；当启发式堆叠过多时，算法结果与复杂度会变得难以预测。作者从基本演算出发，逐步扩展到 Coq 实际实现的完整 CIC，给出一个支持宇宙多态、规范结构（Coq 合一中的重载机制）和少量有用启发式的新合一算法的完整描述。作者还实现了该算法，并在多个库上进行测试，结果表明所选启发式足以支撑大型开发。
Abstract Unification is a core component of every proof assistant or programming language featuring dependent types. In many cases, it must deal with higher order problems up to conversion. Since unification in such conditions is undecidable, unification algorithms may include several heuristics to solve common problems. However, when the stack of heuristics grows large, the result and complexity of the algorithm can become unpredictable. Our contributions are twofold: (1) We present a full description of a new unification algorithm for the Calculus of Inductive Constructions (the base logic of C OQ ), building it up from a basic calculus to the full Calculus of Inductive Constructions as it is implemented in C OQ , including universe polymorphism, canonical structures (the overloading mechanism baked into C OQ 's unification), and a small set of useful heuristics. (2) We implemented our algorithm, and tested it on several libraries, providing evidence that the selected set of heuristics suffices for large developments.
@article{ZilianiS17,
title = {A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading},
author = {BETA ZILIANI and MATTHIEU SOZEAU},
journal = {Journal of Functional Programming},
volume = {27},
year = {2017},
doi = {10.1017/s0956796817000028}
}