A unification algorithm for Coq featuring 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), 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.
Type de document :
Communication dans un congrès
20th ACM SIGPLAN International Conference on Functional Programming, Sep 2015, Vancouver, Canada. ICFP 2015 Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, 〈10.1145/2784731.2784751〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01248804
Contributeur : Matthieu Sozeau <>
Soumis le : lundi 28 décembre 2015 - 18:57:22
Dernière modification le : jeudi 11 janvier 2018 - 06:22:37

Identifiants

Collections

INRIA | PPS | USPC

Citation

Beta Ziliani, Matthieu Sozeau. A unification algorithm for Coq featuring universe polymorphism and overloading. 20th ACM SIGPLAN International Conference on Functional Programming, Sep 2015, Vancouver, Canada. ICFP 2015 Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, 〈10.1145/2784731.2784751〉. 〈hal-01248804〉

Partager

Métriques

Consultations de la notice

103