{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,5]],"date-time":"2026-05-05T12:30:22Z","timestamp":1777984222711,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":33,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,1,14]],"date-time":"2015-01-14T00:00:00Z","timestamp":1421193600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["KAKENHI 25280024"],"award-info":[{"award-number":["KAKENHI 25280024"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2015,1,14]]},"DOI":"10.1145\/2676726.2676996","type":"proceedings-article","created":{"date-parts":[[2014,12,19]],"date-time":"2014-12-19T08:51:05Z","timestamp":1418979065000},"page":"195-207","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Manifest Contracts for Datatypes"],"prefix":"10.1145","author":[{"given":"Taro","family":"Sekiyama","sequence":"first","affiliation":[{"name":"Kyoto University, Kyoto, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuki","family":"Nishida","sequence":"additional","affiliation":[{"name":"Kyoto University, Kyoto, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Atsushi","family":"Igarashi","sequence":"additional","affiliation":[{"name":"Kyoto University, Kyoto, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,1,14]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"The Agda 2 homepage. http:\/\/wiki.portal.chalmers.se\/ agda\/pmwiki.php.  The Agda 2 homepage. http:\/\/wiki.portal.chalmers.se\/ agda\/pmwiki.php."},{"key":"e_1_3_2_2_2_1","unstructured":"The Coq proof assistant. http:\/\/coq.inria.fr\/.  The Coq proof assistant. http:\/\/coq.inria.fr\/."},{"key":"e_1_3_2_2_3_1","volume-title":"Refining inductive types. Logical Methods in Computer Science, 8(2:9):1--30","author":"Atkey R.","year":"2012","unstructured":"R. Atkey , P. Johann , and N. Ghani . Refining inductive types. Logical Methods in Computer Science, 8(2:9):1--30 , 2012 . R. Atkey, P. Johann, and N. Ghani. Refining inductive types. Logical Methods in Computer Science, 8(2:9):1--30, 2012."},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1987211.1987213"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863560"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806005971"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1929501.1929527"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581484"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85373-2_7"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111059"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_3_2_2_13_1","unstructured":"M. Greenberg. Manifest Contracts. PhD thesis University of Pennsylvania 2013.   M. Greenberg. Manifest Contracts. PhD thesis University of Pennsylvania 2013."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706341"},{"key":"e_1_3_2_2_15_1","first-page":"93","volume-title":"Scheme and Functional Programming Workshop","author":"Gronski J.","year":"2006","unstructured":"J. Gronski , K. Knowles , A. Tomb , S. N. Freund , and C. Flanagan . Sage: Hybrid checking for flexible specifications . In Scheme and Functional Programming Workshop , pages 93 -- 104 , 2006 . J. Gronski, K. Knowles, A. Tomb, S. N. Freund, and C. Flanagan. Sage: Hybrid checking for flexible specifications. In Scheme and Functional Programming Workshop, pages 93--104, 2006."},{"key":"e_1_3_2_2_16_1","volume-title":"Trends in Functional Prog. (TFP)","author":"Herman D.","year":"2007","unstructured":"D. Herman , A. Tomb , and C. Flanagan . Space-efficient gradual typing . In Trends in Functional Prog. (TFP) , 2007 . D. Herman, A. Tomb, and C. Flanagan. Space-efficient gradual typing. In Trends in Functional Prog. (TFP), 2007."},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542510"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1667048.1667051"},{"key":"e_1_3_2_2_19_1","volume-title":"UCSC","author":"Knowles K.","year":"2007","unstructured":"K. Knowles , A. Tomb , J. Gronski , S. N. Freund , and C. Flanagan . Sage: Unified hybrid checking for first-class types, general refinement types, and dynamic (extended report). Technical report , UCSC , 2007 . K. Knowles, A. Tomb, J. Gronski, S. N. Freund, and C. Flanagan. Sage: Unified hybrid checking for first-class types, general refinement types, and dynamic (extended report). Technical report, UCSC, 2007."},{"key":"e_1_3_2_2_20_1","volume-title":"Funct. Program.","author":"McBride C.","year":"2014","unstructured":"C. McBride . Ornamental algebras, algebraic ornaments. J . Funct. Program. , 2014 . To appear. C. McBride. Ornamental algebras, algebraic ornaments. J. Funct. Program., 2014. To appear."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/534929"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628156"},{"key":"e_1_3_2_2_23_1","volume-title":"The MIT Press","author":"Pierce B. C.","year":"2002","unstructured":"B. C. Pierce . Types and Programming Languages . The MIT Press , Cambridge, MA, USA , 2002 . ISBN 0--262--16209--1. B. C. Pierce. Types and Programming Languages. The MIT Press, Cambridge, MA, USA, 2002. ISBN 0--262--16209--1."},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706342"},{"key":"e_1_3_2_2_26_1","series-title":"LNCS","first-page":"1","volume-title":"Proc. of ACM FPCA","author":"Turner D. A.","year":"1985","unstructured":"D. A. Turner . Miranda: A non-strict functional language with poly- morphic types . In Proc. of ACM FPCA , volume 201 of LNCS , pages 1 -- 16 , 1985 . D. A. Turner. Miranda: A non-strict functional language with poly- morphic types. In Proc. of ACM FPCA, volume 201 of LNCS, pages 1--16, 1985."},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_13"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006216"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103746.2103767"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480889"}],"event":{"name":"POPL '15: The 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Mumbai India","acronym":"POPL '15","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2676726.2676996","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2676726.2676996","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:03Z","timestamp":1750212783000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2676726.2676996"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,1,14]]},"references-count":33,"alternative-id":["10.1145\/2676726.2676996","10.1145\/2676726"],"URL":"https:\/\/doi.org\/10.1145\/2676726.2676996","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2775051.2676996","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2015,1,14]]},"assertion":[{"value":"2015-01-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}