HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Journal articles

A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading

Beta Ziliani 1 Matthieu Sozeau 2
2 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
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 COQ), building it up from a basic calculus to the full Calculus of Inductive Constructions as it is implemented in COQ, including universe polymorphism, canonical structures (the overloading mechanism baked into COQ'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.
Document type :
Journal articles
Complete list of metadata

Contributor : Matthieu Sozeau Connect in order to contact the contributor
Submitted on : Friday, December 22, 2017 - 5:24:22 PM
Last modification on : Friday, January 21, 2022 - 3:14:14 AM




Beta Ziliani, Matthieu Sozeau. A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading. Journal of Functional Programming, Cambridge University Press (CUP), 2017, 27, ⟨10.1017/S0956796817000028⟩. ⟨hal-01671925⟩



Record views