System F with Coercion Constraints

Julien Cretin 1 Didier Rémy 1, *
* Auteur correspondant
Abstract : We present a second-order λ-calculus with coercion constraints that generalizes a previous extension of System F with paramet-ric coercion abstractions by allowing multiple but simultaneous type and coercion abstractions, as well as recursive coercions and equi-recursive types. This enables a uniform presentation of several type system features that had previously been studied separately: type containment, bounded and instance-bounded polymorphism, which are already encodable with parametric coercion abstraction, and ML-style subtyping constraints. Our framework allows for a clear separation of language constructs with and without compu-tational content. We also distinguish coherent coercions that are fully erasable from potentially incoherent coercions that suspend the evaluation—and enable the encoding of GADTs. Technically, type coercions that witness subtyping relations be-tween types are replaced by a more expressive notion of typing co-ercions that witness subsumption relations between typings, e.g. pairs composed of a typing environment and a type. Our calcu-lus is equipped with full reduction that allows reduction under abstractions—but we also introduce a form of weak reduction as reduction cannot proceed under incoherent type abstractions. Type soundness is proved by adapting the step-indexed semantics tech-nique to full reduction, moving indices inside terms so as to control the reduction steps internally—but this is only detailed in the ex-tended version.
Type de document :
Communication dans un congrès
Thomas A. Henzinger; Dale Miller. CSL-LICS 2014: Joint Meeting of the Annual Conference on Computer Science Logic and the Annual Symposium on Logic in Computer Science, Jul 2014, Vienna, Austria. ACM, pp.34, 2014, <10.1145/2603088.2603128>
Liste complète des métadonnées

https://hal.inria.fr/hal-01093239
Contributeur : Didier Rémy <>
Soumis le : mercredi 10 décembre 2014 - 13:57:29
Dernière modification le : mercredi 14 décembre 2016 - 01:07:55
Document(s) archivé(s) le : mercredi 11 mars 2015 - 11:05:43

Fichier

Cretin-Remy!fcc@lics2014.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Julien Cretin, Didier Rémy. System F with Coercion Constraints. Thomas A. Henzinger; Dale Miller. CSL-LICS 2014: Joint Meeting of the Annual Conference on Computer Science Logic and the Annual Symposium on Logic in Computer Science, Jul 2014, Vienna, Austria. ACM, pp.34, 2014, <10.1145/2603088.2603128>. <hal-01093239>

Partager

Métriques

Consultations de
la notice

66

Téléchargements du document

49