A calculus of constructions with explicit subtyping

Abstract : The calculus of constructions can be extended with an infinite hierarchy of universes and cumulative subtyping. In this hierarchy, each universe is contained in a higher universe. Subtyping is usually left implicit in the typing rules. We present an alternative version of the calculus of constructions where subtyping is explicit. This new system avoids problems related to coercions and dependent types by using the Tarski style of universes and by introducing additional equations to reflect equality.
Type de document :
Communication dans un congrès
Hugo Herbelin; Pierre Letouzey; Matthieu Sozeau. 20th International Conference on Types for Proofs and Programs (TYPES 2014), May 2014, Institut Henri Poincaré, Paris, France. 39, 2015, LIPICS
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

https://hal.archives-ouvertes.fr/hal-01097401
Contributeur : Ali Assaf <>
Soumis le : jeudi 14 janvier 2016 - 02:05:59
Dernière modification le : vendredi 15 janvier 2016 - 01:14:20
Document(s) archivé(s) le : jeudi 10 novembre 2016 - 22:54:13

Fichier

coc-explicit-subtyping-types-2...
Fichiers éditeurs autorisés sur une archive ouverte

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

  • HAL Id : hal-01097401, version 2

Collections

Citation

Ali Assaf. A calculus of constructions with explicit subtyping. Hugo Herbelin; Pierre Letouzey; Matthieu Sozeau. 20th International Conference on Types for Proofs and Programs (TYPES 2014), May 2014, Institut Henri Poincaré, Paris, France. 39, 2015, LIPICS. 〈hal-01097401v2〉

Partager

Métriques

Consultations de la notice

136

Téléchargements de fichiers

88