{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:12:36Z","timestamp":1770275556091,"version":"3.49.0"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2017,2,6]],"date-time":"2017-02-06T00:00:00Z","timestamp":1486339200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"JSPS Grant-in-Aid for Scientific Research","award":["25280024"],"award-info":[{"award-number":["25280024"]}]},{"name":"MEXT of Japan"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2017,3,31]]},"abstract":"<jats:p>\n            Manifest contracts track precise program properties by refining types with predicates\u2014for example, {\n            <jats:italic>x<\/jats:italic>\n            :Int\u2223\n            <jats:italic>x<\/jats:italic>\n            &gt; 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\u2014 for instance, an abstract type of stacks might specify that the pop operation has input type {\n            <jats:italic>x<\/jats:italic>\n            :\u03b1 Stack \u2223 not (empty\n            <jats:italic>x<\/jats:italic>\n            )}.\n          <\/jats:p>\n          <jats:p>\n            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 S\n            <jats:sc>age<\/jats:sc>\n            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\u2014it resolves the issues in prior calculi with delayed substitution on casts.\n          <\/jats:p>","DOI":"10.1145\/2994594","type":"journal-article","created":{"date-parts":[[2017,2,10]],"date-time":"2017-02-10T13:28:54Z","timestamp":1486733334000},"page":"1-36","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Polymorphic Manifest Contracts, Revised and Resolved"],"prefix":"10.1145","volume":"39","author":[{"given":"Taro","family":"Sekiyama","sequence":"first","affiliation":[{"name":"Kyoto University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Atsushi","family":"Igarashi","sequence":"additional","affiliation":[{"name":"Kyoto University, Kyoto, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Greenberg","sequence":"additional","affiliation":[{"name":"Pomona College, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,2,6]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000186"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75296"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1570506.1570507"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926409"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/162552.162561"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/1987211.1987213"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863560"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384659"},{"key":"e_1_2_2_12_1","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism","author":"de Bruijn Nicolaas G.","unstructured":"Nicolaas G. de Bruijn. 1980. A survey of the project Automath. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, J. P. Seldin and J. R. Hindley (Eds.). Academic Press, Cambridge, MA, 579--606."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581484"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111059"},{"key":"e_1_2_2_16_1","volume-title":"Reference: Racket. Technical Report PLT-TR-2010-1. PLT Design","author":"Flatt Matthew","year":"2010","unstructured":"Matthew Flatt and PLT. 2010. Reference: Racket. Technical Report PLT-TR-2010-1. PLT Design. http:\/\/racket-lang.org\/tr1\/."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/2604521"},{"key":"e_1_2_2_19_1","volume-title":"Retrieved","author":"Greenberg Michael","year":"2015","unstructured":"Michael Greenberg. 2015a. Combining Manifest Contracts with State. Retrieved January 18, 2017, from http:\/\/www.cs.pomona.edu\/&sim;michael\/papers\/hope2015.pdf."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676967"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706341"},{"key":"e_1_2_2_22_1","volume-title":"Proceedings of the Conference on Trends in Functional Programming (TFP\u201907)","author":"Gronski Jessica","year":"2007","unstructured":"Jessica Gronski and Cormac Flanagan. 2007. Unifying hybrid types and contracts. In Proceedings of the Conference on Trends in Functional Programming (TFP\u201907). 54--70."},{"key":"e_1_2_2_23_1","volume-title":"Proceedings of the Scheme and Functional Programming Workshop.","author":"Gronski Jessica","year":"2006","unstructured":"Jessica Gronski, Kenneth Knowles, Aaron Tomb, Stephen N. Freund, and Cormac Flanagan. 2006. Sage: Hybrid checking for flexible specifications. In Proceedings of the Scheme and Functional Programming Workshop."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/371880.371887"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297081.1297089"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/145055.145092"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-011-9066-z"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2541568.2541569"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542510"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908091"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481848.1481853"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1667048.1667051"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944725"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792878.1792881"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/318593.318606"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/2685048.2685063"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/512927.512938"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159812"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596572"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628156"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/1-4020-8141-3_34"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/645891.671440"},{"key":"e_1_2_2_46_1","unstructured":"Benjamin Pierce and Eijiro Sumii. 2000. Relating cryptography and polymorphism. Unpublished Manuscript. http:\/\/www.cis.upenn.edu\/&sim;bcpierce\/papers\/infohide.ps."},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500003066"},{"key":"e_1_2_2_48_1","volume-title":"Proceedings of the IFIP Congress. 513--523","author":"Reynolds John C.","year":"1983","unstructured":"John C. Reynolds. 1983. Types, abstraction and parametric polymorphism. In Proceedings of the IFIP Congress. 513--523."},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_2_2_50_1","unstructured":"Taro Sekiyama and Atsushi Igarashi. 2012. Logical Relations for a Manifest Contract Calculus Fixed (talk abstract and slides). Available at http:\/\/hope2012.mpi-sws.org\/."},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676996"},{"key":"e_1_2_2_52_1","volume-title":"Proceedings of the Scheme and Functional Programming Workshop.","author":"Jeremy","unstructured":"Jeremy G. Siek and Walid Taha. 2006. Gradual typing for functional languages. In Proceedings of the Scheme and Functional Programming Workshop."},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384674"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1176617.1176755"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863561"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","unstructured":"Philip Wadler. 1989. Theorems for free! In Proceedings of the Conference on Functional Programming and Computer Architecture (FPCA\u201989). 347--359. 10.1145\/99370.99404","DOI":"10.1145\/99370.99404"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_1"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604150"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2994594","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2994594","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:39:48Z","timestamp":1750217988000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2994594"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,2,6]]},"references-count":57,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,3,31]]}},"alternative-id":["10.1145\/2994594"],"URL":"https:\/\/doi.org\/10.1145\/2994594","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,2,6]]},"assertion":[{"value":"2015-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-02-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}