Universe Polymorphism in Coq

Matthieu Sozeau 1, 2 Nicolas Tabareau 3, 4
1 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
3 ASCOLA - Aspect and composition languages
Inria Rennes – Bretagne Atlantique , Département informatique - EMN, LINA - Laboratoire d'Informatique de Nantes Atlantique
Abstract : Universes are used in Type Theory to ensure consistency by checking that definitions are well-stratified according to a certain hierarchy. In the case of the Coq proof assistant, based on the predicative Calculus of Inductive Constructions (pCIC), this hierachy is built from an impredicative sort Prop and an infinite number of predicative Type_i universes. A cumulativity relation represents the inclusion order of uni- verses in the core theory. Originally, universes were thought to be floating levels, and definitions to implicitly constrain these levels in a consistent manner. This works well for most theories, however the globality of levels and constraints precludes generic constructions on universes that could work at different levels. Universe polymorphism extends this setup by adding local bindings of universes and constraints, supporting generic definitions over universes, reusable at different levels. This provides the same kind of code reuse facilities as ML-style parametric polymorphism. However, the structure and hierarchy of universes is more complex than bare polymorphic type variables. In this paper, we introduce a conservative extension of pCIC supporting universe polymorphism and treating its whole hierarchy. This new design supports typical ambiguity and implicit polymorphic generalization at the same time, keeping it mostly transparent to the user. Benchmarking the implementation as an extension of the Coq proof assistant on real-world examples gives encouraging results.
Type de document :
Communication dans un congrès
Interactive Theorem Proving, Jul 2014, Vienna, Austria. 2014
Liste complète des métadonnées

https://hal.inria.fr/hal-00974721
Contributeur : Nicolas Tabareau <>
Soumis le : lundi 7 avril 2014 - 13:36:33
Dernière modification le : mardi 4 décembre 2018 - 11:08:03

Identifiants

  • HAL Id : hal-00974721, version 1

Citation

Matthieu Sozeau, Nicolas Tabareau. Universe Polymorphism in Coq. Interactive Theorem Proving, Jul 2014, Vienna, Austria. 2014. 〈hal-00974721〉

Partager

Métriques

Consultations de la notice

403