Subtyping recursive types Export

@article{citeulike:4499633, abstract = {We investigate the interactions of subtyping and recursive types, in a simply typed \&lgr;-calculus. The two fundamental questions here are whether two (recursive)types are in the subtype relation and whether a term has a type. To address the first question, we relate various definitions of type equivalence and subtyping that are induced by a model, an ordering on infinite trees, an algorithm, and a set of type rules. We show soundness and completeness among the rules, the algorithm, and the tree semantics. We also prove soundness and a restricted form of completeness for the model. To address the second question, we show that to every pair of types in the subtype relation we can associate a term whose denotation is the uniquely determined coercion map between the two types. Moreover, we derive an algorithm that, when given a term with implicit coercions, can infer its least type whenever possible.}, address = {New York, NY, USA}, author = {Amadio, Roberto M. and Cardelli, Luca}, citeulike-article-id = {4499633}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=155231}, citeulike-linkout-1 = {http://dx.doi.org/10.1145/155183.155231}, doi = {10.1145/155183.155231}, issn = {0164-0925}, journal = {ACM Trans. Program. Lang. Syst.}, keywords = {type-theory}, number = {4}, pages = {575--631}, posted-at = {2009-05-30 06:42:18}, priority = {2}, publisher = {ACM}, title = {Subtyping recursive types}, url = {http://dx.doi.org/10.1145/155183.155231}, volume = {15}, year = {1993} }

TY - JOUR ID - citeulike:4499633 L3 - citeulike-article-id:4499633 N2 - We investigate the interactions of subtyping and recursive types, in a simply typed &lgr;-calculus. The two fundamental questions here are whether two (recursive)types are in the subtype relation and whether a term has a type. To address the first question, we relate various definitions of type equivalence and subtyping that are induced by a model, an ordering on infinite trees, an algorithm, and a set of type rules. We show soundness and completeness among the rules, the algorithm, and the tree semantics. We also prove soundness and a restricted form of completeness for the model. To address the second question, we show that to every pair of types in the subtype relation we can associate a term whose denotation is the uniquely determined coercion map between the two types. Moreover, we derive an algorithm that, when given a term with implicit coercions, can infer its least type whenever possible. IS - 4 JF - ACM Trans. Program. Lang. Syst. SN - 0164-0925 AD - New York, NY, USA EP - 631 TI - Subtyping recursive types PB - ACM VL - 15 SP - 575 KW - type-theory AU - Amadio, Roberto AU - Cardelli, Luca PY - 1993/// UR - http://dx.doi.org/10.1145/155183.155231 ER -