TY - JOUR
T1 - Polymorphic manifest contracts, revised and resolved
AU - Sekiyama, Taro
AU - Igarashi, Atsushi
AU - Greenberg, Michael
N1 - Publisher Copyright:
© 2017 ACM.
PY - 2017/2
Y1 - 2017/2
N2 - Manifest contracts track precise program properties by refining types with predicates-for example, {x:Int | x > 0} denotes the positive integers. Contracts and polymorphism make a natural combination: programmers can give strong contracts to abstract types, precisely stating pre- and post conditions while hiding implementation details-for instance, an abstract type of stacks might specify that the pop operation has input type {x:αStack | not (empty x)}. This article studies a polymorphic calculus with manifest contracts and establishes fundamental properties including type soundness and relational parametricity. Indeed, this is not the first work on polymorphic manifest contracts, but existing calculi are not very satisfactory. Gronski et al. developed the SAGE language, which introduces polymorphism through the Type:Type discipline, but they do not study parametricity. Some authors of this article have produced two separate works: Belo et al. [2011] and Greenberg [2013] studied polymorphic manifest contracts and parametricity, but their calculi have metatheoretical problems in the type conversion relations. Indeed, they depend on a few conjectures, which turn out to be false. Our calculus is the first polymorphic manifest calculus with parametricity, depending on no conjectures-it resolves the issues in prior calculi with delayed substitution on casts.
AB - Manifest contracts track precise program properties by refining types with predicates-for example, {x:Int | x > 0} denotes the positive integers. Contracts and polymorphism make a natural combination: programmers can give strong contracts to abstract types, precisely stating pre- and post conditions while hiding implementation details-for instance, an abstract type of stacks might specify that the pop operation has input type {x:αStack | not (empty x)}. This article studies a polymorphic calculus with manifest contracts and establishes fundamental properties including type soundness and relational parametricity. Indeed, this is not the first work on polymorphic manifest contracts, but existing calculi are not very satisfactory. Gronski et al. developed the SAGE language, which introduces polymorphism through the Type:Type discipline, but they do not study parametricity. Some authors of this article have produced two separate works: Belo et al. [2011] and Greenberg [2013] studied polymorphic manifest contracts and parametricity, but their calculi have metatheoretical problems in the type conversion relations. Indeed, they depend on a few conjectures, which turn out to be false. Our calculus is the first polymorphic manifest calculus with parametricity, depending on no conjectures-it resolves the issues in prior calculi with delayed substitution on casts.
KW - Abstract datatypes
KW - Contracts
KW - Corrections
KW - Dynamic checking
KW - Logical relations
KW - Parametric polymorphism
KW - Postconditions
KW - Preconditions
KW - Refinement types
KW - Runtime verification
KW - Syntactic proof
UR - http://www.scopus.com/inward/record.url?scp=85012284859&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85012284859&partnerID=8YFLogxK
U2 - 10.1145/2994594
DO - 10.1145/2994594
M3 - Article
AN - SCOPUS:85012284859
SN - 0164-0925
VL - 39
JO - ACM Transactions on Programming Languages and Systems
JF - ACM Transactions on Programming Languages and Systems
IS - 1
M1 - 3
ER -