{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:31:29Z","timestamp":1767929489957,"version":"3.49.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-11-LABEX-0045-DIGICOSME"],"award-info":[{"award-number":["ANR-11-LABEX-0045-DIGICOSME"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,1,16]]},"abstract":"<jats:p>\n            We extend classic union and intersection type systems with a type-case construction and show that the combination of the union elimination rule of the former and the typing rules for type-cases of our extension encompasses\n            <jats:italic>occurrence typing<\/jats:italic>\n            . To apply this system in practice, we define a canonical form for the expressions of our extension, called MSC-form. We show that an expression of the extension is typable if and only if its MSC-form is, and reduce the problem of typing the latter to the one of reconstructing annotations for that term. We provide a sound algorithm that performs this reconstruction and a proof-of-concept implementation.\n          <\/jats:p>","DOI":"10.1145\/3498674","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["On type-cases, union elimination, and occurrence typing"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0951-7535","authenticated-orcid":false,"given":"Giuseppe","family":"Castagna","sequence":"first","affiliation":[{"name":"CNRS, France \/ Universit\u00e9 de Paris, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1590-2392","authenticated-orcid":false,"given":"Micka\u00ebl","family":"Laurent","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Paris, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1729-870X","authenticated-orcid":false,"given":"Kim","family":"Nguy\u1ec5n","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Saclay, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2904-5099","authenticated-orcid":false,"given":"Matthew","family":"Lutze","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Paris, France"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1086"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(1:15)2020"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110285"},{"key":"e_1_2_2_4_1","volume-title":"Revisiting Occurrence Typing. oct, arXiv:1907.05590. To appear in Science of Computer Programming","author":"Castagna Giuseppe","unstructured":"Giuseppe Castagna , Victor Lanvin , Micka\u00ebl Laurent , and Kim Nguy\u1ec5n . 2021. Revisiting Occurrence Typing. oct, arXiv:1907.05590. To appear in Science of Computer Programming , Elsevier Giuseppe Castagna, Victor Lanvin, Micka\u00ebl Laurent, and Kim Nguy\u1ec5n. 2021. Revisiting Occurrence Typing. oct, arXiv:1907.05590. To appear in Science of Computer Programming, Elsevier"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290329"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3462306"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676991"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676991"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951928"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034788"},{"key":"e_1_2_2_11_1","unstructured":"The CDuce Compiler. https:\/\/www.cduce.org  The CDuce Compiler. https:\/\/www.cduce.org"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9225-2"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133872"},{"key":"e_1_2_2_14_1","unstructured":"Mariangiola Dezani-Ciancaglini. 2020. Personal communication  Mariangiola Dezani-Ciancaglini. 2020. Personal communication"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80492-4"},{"key":"e_1_2_2_16_1","volume-title":"abs\/1908.05839","author":"Dunfield Jana","year":"2019","unstructured":"Jana Dunfield and Neel Krishnaswami . 2019. Bidirectional Typing . CoRR , abs\/1908.05839 ( 2019 ), arxiv:1908.05839. Jana Dunfield and Neel Krishnaswami. 2019. Bidirectional Typing. CoRR, abs\/1908.05839 (2019), arxiv:1908.05839."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290322"},{"key":"e_1_2_2_18_1","unstructured":"Flow. https:\/\/flow.org\/  Flow. https:\/\/flow.org\/"},{"key":"e_1_2_2_19_1","unstructured":"Alain Frisch. 2004. Th\u00e9orie conception et r\u00e9alisation d\u2019un langage de programmation adapt\u00e9 \u00e0 XML. Ph. D. Dissertation. Universit\u00e9 Paris Diderot. http:\/\/www.cduce.org\/papers\/frisch_phd.pdf  Alain Frisch. 2004. Th\u00e9orie conception et r\u00e9alisation d\u2019un langage de programmation adapt\u00e9 \u00e0 XML. Ph. D. Dissertation. Universit\u00e9 Paris Diderot. http:\/\/www.cduce.org\/papers\/frisch_phd.pdf"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029823"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1391289.1391293"},{"key":"e_1_2_2_22_1","volume-title":"Seldin","author":"Roger Hindley J.","year":"2008","unstructured":"J. Roger Hindley and Jonathan P . Seldin . 2008 . Lambda-Calculus and Combinators An Introduction. Cambridge University Press . isbn:978-0-521-89885-0 J. Roger Hindley and Jonathan P. Seldin. 2008. Lambda-Calculus and Combinators An Introduction. Cambridge University Press. isbn:978-0-521-89885-0"},{"key":"e_1_2_2_23_1","volume-title":"Advanced Logical Type Systems for Untyped Languages. Ph. D. Dissertation","author":"Kent Andrew M.","unstructured":"Andrew M. Kent . 2019. Advanced Logical Type Systems for Untyped Languages. Ph. D. Dissertation . Indiana University . https:\/\/pnwamk.github.io\/docs\/dissertation.pdf Andrew M. Kent. 2019. Advanced Logical Type Systems for Untyped Languages. Ph. D. Dissertation. Indiana University. https:\/\/pnwamk.github.io\/docs\/dissertation.pdf"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(86)80019-5"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-011-0834-8_5"},{"key":"e_1_2_2_26_1","unstructured":"TypeScript. https:\/\/www.typescriptlang.org\/  TypeScript. https:\/\/www.typescriptlang.org\/"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111058"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676971"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/141471.141563"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328486"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863561"},{"key":"e_1_2_2_35_1","unstructured":"2019. What exactly should we call syntax-directed inference rules? Discussion on the Types mailing list. http:\/\/lists.seas.upenn.edu\/pipermail\/types-list\/2019\/002138.html  2019. What exactly should we call syntax-directed inference rules? Discussion on the Types mailing list. http:\/\/lists.seas.upenn.edu\/pipermail\/types-list\/2019\/002138.html"},{"key":"e_1_2_2_36_1","volume-title":"Peter Parker principle. https:\/\/en.wikipedia.org\/wiki\/With_great_power_comes_great_responsibility [Online","year":"2021","unstructured":"Wikipedia. 2021. Peter Parker principle. https:\/\/en.wikipedia.org\/wiki\/With_great_power_comes_great_responsibility [Online ; accessed 22- October - 2021 ] Wikipedia. 2021. Peter Parker principle. https:\/\/en.wikipedia.org\/wiki\/With_great_power_comes_great_responsibility [Online; accessed 22-October-2021]"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498674","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498674","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:28Z","timestamp":1750188628000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498674"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":36,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498674"],"URL":"https:\/\/doi.org\/10.1145\/3498674","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}