From Amber to Coercion Constraints

Abstract : Subtyping is a common tool in the design of type systems that finds itsroots in the eta-expansion of arrow types and the notion of typecontainment obtained by closing System Fby eta-expansion. Althoughstrongly related, subtyping and type containment still significantlydiffer from one another when put into practice. We introduce coercionconstraints to relate and generalize subtyping and type containment aswell as all variants of F-bounded quantification and instance-boundedquantification used for first-order type inference in the presence ofsecond-order types. We obtain a type system with a clearer separationbetween computational and erasable parts of terms.
Type de document :
Chapitre d'ouvrage
Martin Abadi; Philippa Gardner; Andrew D. Gordon; Radu Mardare. Essays for the Luca Cardelli Fest, Microsoft Research, 2014, TechReport, <http://research.microsoft.com/pubs/226237/Luca-Cardelli-Fest-MSR-TR-2014-104.pdf>
Liste complète des métadonnées


https://hal.inria.fr/hal-01093216
Contributeur : Didier Rémy <>
Soumis le : mercredi 10 décembre 2014 - 18:28:58
Dernière modification le : mercredi 14 décembre 2016 - 01:07:56
Document(s) archivé(s) le : mercredi 11 mars 2015 - 11:01:05

Fichier

DidierRemyCoercions.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01093216, version 1

Collections

Citation

Didier Rémy, Julien Cretin. From Amber to Coercion Constraints. Martin Abadi; Philippa Gardner; Andrew D. Gordon; Radu Mardare. Essays for the Luca Cardelli Fest, Microsoft Research, 2014, TechReport, <http://research.microsoft.com/pubs/226237/Luca-Cardelli-Fest-MSR-TR-2014-104.pdf>. <hal-01093216>

Partager

Métriques

Consultations de
la notice

66

Téléchargements du document

78