{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,14]],"date-time":"2026-05-14T11:17:27Z","timestamp":1778757447858,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":24,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-1422133"],"award-info":[{"award-number":["CCF-1422133"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,1]]},"DOI":"10.1145\/3009837.3009901","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T16:20:29Z","timestamp":1482423629000},"page":"374-386","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Deciding equivalence with sums and the empty type"],"prefix":"10.1145","author":[{"given":"Gabriel","family":"Scherer","sequence":"first","affiliation":[{"name":"Northeastern University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,1]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Deciding coproduct equality with focusing. Online draft","author":"Ahmad Arbob","year":"2010","unstructured":"Arbob Ahmad, Daniel R. Licata, and Robert Harper. Deciding coproduct equality with focusing. Online draft, 2010."},{"key":"e_1_3_2_1_2_1","volume-title":"FLOPS","author":"Altenkirch Thorsten","year":"2004","unstructured":"Thorsten Altenkirch and Tarmo Uustalu. Normalization by evaluation for lambda-2. In FLOPS, 2004."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/871816.871869"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Jean-Marc Andreoli. Logic Programming with Focusing Proof in Linear Logic. Journal of Logic and Computation 2(3) 1992.","DOI":"10.1093\/logcom\/2.3.297"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964007"},{"key":"e_1_3_2_1_6_1","first-page":"696119","author":"B\u00f6hm Corrado","year":"1968","unstructured":"Corrado B\u00f6hm. Alcune proprieta delle forme normali nel k-calcolo. IAC Pubbl, 696119, 1968.","journal-title":"IAC Pubbl"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-09680-3_26"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9091-0"},{"key":"e_1_3_2_1_9_1","volume-title":"CSL","author":"Chaudhuri Kaustuv","year":"2012","unstructured":"Kaustuv Chaudhuri, Stefan Hetzl, and Dale Miller. A Systematic Approach to Canonicity in the Classical Sequent Calculus. In CSL, 2012."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837652"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2833"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/645894.671754"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0064870"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/645892.671593"},{"key":"e_1_3_2_1_15_1","volume-title":"The exp-log normal form of types and canonical terms for lambda calculus with sums. CoRR, arxiv:1502.04634","author":"Ilik Danko","year":"2015","unstructured":"Danko Ilik. The exp-log normal form of types and canonical terms for lambda calculus with sums. CoRR, arxiv:1502.04634, 2015. URL http:\/\/arxiv.org\/abs\/1502.04634."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/2392389.2392432"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770203.1770222"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.22"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Gabriel Scherer. Which types have a unique inhabitant? Focusing on pure program equivalence. PhD thesis Universit\u00e9 Paris-Diderot 2016.","DOI":"10.1145\/2784731.2784757"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784757"},{"key":"e_1_3_2_1_21_1","volume-title":"Structural focalization. CoRR, arxiv:1109.6273","author":"Simmons Robert J.","year":"2011","unstructured":"Robert J. Simmons. Structural focalization. CoRR, arxiv:1109.6273, 2011. URL http:\/\/arxiv.org\/abs\/1109.6273."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/645892.671581"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273377"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/1714175"}],"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.3009901","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3009837.3009901","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3009837.3009901","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:42:56Z","timestamp":1763458976000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009901"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1]]},"references-count":24,"alternative-id":["10.1145\/3009837.3009901","10.1145\/3009837"],"URL":"https:\/\/doi.org\/10.1145\/3009837.3009901","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3093333.3009901","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"}}]}}