Name
Abstract | ||
|---|---|---|
We present a second-order λ-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 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 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 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 technique to full reduction, moving indices inside terms so as to control the reduction steps internally---but this is only detailed in the extended version. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1145/2603088.2603128 | CSL-LICS |
Keywords | Field | DocType |
design,f-eta,formal definitions and theory,recursive coercions,type constraints,gadts,coercion,full reduction,subtyping,languages,recursive types,type containment,typings,polymorphism,theory,system f,step-indexed semantics,retyping functions,type,bounded polymorphism | Discrete mathematics,Programming language,Computer science,Bounded quantification,Language construct,System F,Typing environment,Theoretical computer science,Soundness,Subtyping,Recursion,Bounded function | Conference |
Citations | PageRank | References |
3 | 0.42 | 13 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Julien Cretin | 1 | 3 | 0.76 |
| Didier Rémy | 2 | 682 | 49.82 |