{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:48:03Z","timestamp":1772164083226,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,1]]},"DOI":"10.1145\/3009837.3009865","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T16:20:29Z","timestamp":1482423629000},"page":"804-817","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Sums of uncertainty: refinements go gradual"],"prefix":"10.1145","author":[{"given":"Khurram A.","family":"Jafery","sequence":"first","affiliation":[{"name":"University of British Columbia, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jana","family":"Dunfield","sequence":"additional","affiliation":[{"name":"University of British Columbia, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,1]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/103135.103138"},{"key":"e_1_3_2_2_2_1","first-page":"214","volume-title":"Principles of Programming Languages","author":"Ahmed Amal","year":"2011","unstructured":"Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. Blame for all. In Principles of Programming Languages, pages 201\u2013214, 2011."},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660222"},{"key":"e_1_3_2_2_4_1","first-page":"295","volume-title":"ICFP","author":"Schwerter Felipe Ba\u00f1ados","year":"2014","unstructured":"Felipe Ba\u00f1ados Schwerter, Ronald Garcia, and \u00c9ric Tanter. A theory of gradual effect systems. In ICFP, pages 283\u2013295, 2014."},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(95)00021-6"},{"key":"e_1_3_2_2_7_1","volume-title":"The Logical Basis of Metaphysics","author":"Dummett Michael","year":"1991","unstructured":"Michael Dummett. The Logical Basis of Metaphysics. Harvard University Press, 1991. The William James Lectures, 1976."},{"key":"e_1_3_2_2_8_1","volume-title":"Carnegie Mellon University, 2007. CMU-CS-07-129. Jana Dunfield. Elaborating evaluation-order polymorphism. In Int'l Conf. Functional Programming, 2015","author":"Dunfield Jana","year":"2013","unstructured":"Jana Dunfield. A Unified System of Type Refinements. PhD thesis, Carnegie Mellon University, 2007. CMU-CS-07-129. Jana Dunfield. Elaborating evaluation-order polymorphism. In Int'l Conf. Functional Programming, 2015. arXiv:1504.07680 {cs.PL}. Jana Dunfield and Neelakantan R. Krishnaswami. Complete and easy bidirectional typechecking for higher-rank polymorphism. In ICFP, 2013. arXiv:1306.6032 {cs.PL}. Jana Dunfield and Frank Pfenning. Tridirectional typechecking. In Principles of Programming Languages, pages 281-292, 2004."},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676992"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837670"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2678015.2682542"},{"issue":"1","key":"e_1_3_2_2_13_1","first-page":"11","article-title":"On the meanings of the logical constants and the justifications of the logical laws","volume":"1","author":"Martin-L\u00f6f Per","year":"1996","unstructured":"Per Martin-L\u00f6f. On the meanings of the logical constants and the justifications of the logical laws. Nordic Journal of Philosophical Logic, 1(1):11\u201360, 1996. Notes for lectures given in 1983 in Siena, Italy. Trevor L. McDonell, Timothy A. K. Zakian, Matteo Cimini, and Ryan R. Newton. Ghostbuster: A tool for simplifying and converting GADTs. In ICFP, pages 338\u2013350, 2016.","journal-title":"Nordic Journal of Philosophical Logic"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/549659"},{"key":"e_1_3_2_2_15_1","volume-title":"Lecture notes on harmony. Lecture notes for 15\u2013317: Constructive Logic","author":"Pfenning Frank","year":"2009","unstructured":"Frank Pfenning. Lecture notes on harmony. Lecture notes for 15\u2013317: Constructive Logic, Carnegie Mellon University, September 2009."},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003322"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328483"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_2"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268967"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_3_2_2_21_1","volume-title":"Natural Deduction. Almqvist &amp","author":"Prawitz Dag","year":"1965","unstructured":"Dag Prawitz. Natural Deduction. Almqvist & Wiksells, 1965."},{"key":"e_1_3_2_2_22_1","first-page":"27","volume-title":"European Conference on Object-Oriented Programming","author":"Siek Jeremy","unstructured":"Jeremy Siek and Walid Taha. Gradual typing for objects. In European Conference on Object-Oriented Programming, pages 2\u201327. Springer, 2007."},{"key":"e_1_3_2_2_23_1","first-page":"92","volume-title":"Proceedings of the Scheme and Functional Programming Workshop","author":"Jeremy","year":"2006","unstructured":"Jeremy G. Siek and Walid Taha. Gradual typing for functional languages. In Proceedings of the Scheme and Functional Programming Workshop, pages 81\u201392, September 2006."},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1408681.1408688"},{"key":"e_1_3_2_2_25_1","volume-title":"LIPIcs-Leibniz International Proceedings in Informatics","volume":"32","author":"Siek Jeremy G.","year":"2015","unstructured":"Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. Refined criteria for gradual typing. In LIPIcs-Leibniz International Proceedings in Informatics, volume 32. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, 2015."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_1"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"}],"event":{"name":"POPL '17: The 44th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","location":"Paris France","acronym":"POPL '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009865","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3009837.3009865","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:36:22Z","timestamp":1750203382000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009865"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1]]},"references-count":25,"alternative-id":["10.1145\/3009837.3009865","10.1145\/3009837"],"URL":"https:\/\/doi.org\/10.1145\/3009837.3009865","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3093333.3009865","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2017,1]]},"assertion":[{"value":"2017-01-01","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}