Skip to Main content Skip to Navigation
New interface
Reports (Research report)

System F with Coercion Constraints

Abstract : We present a second-order lambda-calculus with coercion constraints that generalizes a previous extension of System F with parametric coercion abstractions by allowing multiple but simultaneous type and coercion abstractions, as well as recursive coercions and equi-recursive types. This allows to present in a uniform way 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 computational 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 between types are replaced by a more expressive notion of typing coercions that witness subsumption relations between typings, e.g. pairs composed of a typing environment and a type. Our calculus is equipped with a strong notion of 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 technique to strong reduction strategies, moving indices inside terms so as to control the reduction steps internally.
Document type :
Reports (Research report)
Complete list of metadata

Cited literature [12 references]  Display  Hide  Download
Contributor : Didier Rémy Connect in order to contact the contributor
Submitted on : Tuesday, January 21, 2014 - 11:18:32 PM
Last modification on : Wednesday, October 26, 2022 - 8:16:16 AM
Long-term archiving on: : Tuesday, April 22, 2014 - 10:15:31 AM


Files produced by the author(s)


  • HAL Id : hal-00934408, version 1



Julien Cretin, Didier Rémy. System F with Coercion Constraints. [Research Report] RR-8456, INRIA. 2014, pp.36. ⟨hal-00934408⟩



Record views


Files downloads