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}
}