{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:43:31Z","timestamp":1780994611940,"version":"3.54.1"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100008398","name":"Villum Fonden","doi-asserted-by":"publisher","award":["25804"],"award-info":[{"award-number":["25804"]}],"id":[{"id":"10.13039\/100008398","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000654","name":"Marie Curie","doi-asserted-by":"publisher","award":["101065303"],"award-info":[{"award-number":["101065303"]}],"id":[{"id":"10.13039\/501100000654","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":[[2024,1,2]]},"abstract":"<jats:p>\n            This paper considers direct encodings of generalized algebraic data types (GADTs) in a minimal suitable lambda-calculus. To this end, we develop an extension of System\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:msub>\n                  <mml:mi mathvariant=\"normal\">F<\/mml:mi>\n                  <mml:mi>\u03c9<\/mml:mi>\n                <\/mml:msub>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            with recursive types and internalized type equalities with injective constant type constructors. We show how GADTs and associated pattern-matching constructs can be directly expressed in the calculus, thus showing that it may be treated as a highly idealized modern functional programming language. We prove that the internalized type equalities in conjunction with injectivity rules increase the expressive power of the calculus by establishing a non-macro-expressibility result in\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:msub>\n                  <mml:mi mathvariant=\"normal\">F<\/mml:mi>\n                  <mml:mi>\u03c9<\/mml:mi>\n                <\/mml:msub>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            , and prove the system type-sound via a syntactic argument. Finally, we build two relational models of our calculus: a simple, unary model that illustrates a novel, two-stage interpretation technique, necessary to account for the equational constraints; and a more sophisticated, binary model that relaxes the construction to allow, for the first time, formal reasoning about data-abstraction in a calculus equipped with GADTs.\n          <\/jats:p>","DOI":"10.1145\/3632866","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"695-723","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["The Essence of Generalized Algebraic Data Types"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5011-3458","authenticated-orcid":false,"given":"Filip","family":"Sieczkowski","sequence":"first","affiliation":[{"name":"Heriot-Watt University, Edinburgh, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7322-5644","authenticated-orcid":false,"given":"Sergei","family":"Stepanenko","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0585-5564","authenticated-orcid":false,"given":"Jonathan","family":"Sterling","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1320-0098","authenticated-orcid":false,"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018613"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2012.46"},{"key":"e_1_3_1_4_1","first-page":"117","volume-title":"Lambda Calculi with Types","author":"Barendregt H. P.","year":"1993","unstructured":"H. P. Barendregt. 1993. Lambda Calculi with Types. Oxford University Press, Inc., USA, 117\u2013309."},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1991.151645"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054285"},{"key":"e_1_3_1_7_1","unstructured":"James Cheney and Ralf Hinze. 2003. First-Class Phantom Types."},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237784"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:16)2011"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290322"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(91)90036-W"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/571157.571161"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782615"},{"key":"e_1_3_1_14_1","unstructured":"Jean-Yves Girard. 1992. A Fixpoint Theorem in Linear Logic. Post to Linear Logic mailing list http:\/\/www.seas.upenn.edu\/~sweirich\/types\/archive\/1992\/msg00030.html."},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000372"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","unstructured":"Patricia Johann and Pierre Cagne. 2022. How Functorial Are (Deep) GADTs? CoRR abs\/2203.14891 (2022). https:\/\/doi.org\/10.48550\/arXiv.2203.14891 10.48550\/arXiv.2203.14891 arXiv:2203.14891","DOI":"10.48550\/arXiv.2203.14891"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328475"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-17(4:23)2021"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3497775.3503680"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.357.6"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159811"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"e_1_3_1_24_1","volume-title":"Sheaves in geometry and logic: a first introduction to topos theory","author":"Lane Saunders Mac","year":"1992","unstructured":"Saunders Mac Lane and Ieke Moerdijk. 1992. Sheaves in geometry and logic: a first introduction to topos theory. Springer."},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037116"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/509043"},{"key":"e_1_3_1_27_1","unstructured":"Piotr Polesiuk. 2017. IxFree: Step-indexed logical relations in Coq. In 3 rd International Workshop on Coq for Programming Languages (CoqPL)."},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111058"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1994.316053"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58025-5_65"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.11.012"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","unstructured":"Filip Sieczkowski Sergei Stepanenko Jonathan Sterling and Lars Birkedal. 2023. The Essence of Generalized Algebraic Data Types. https:\/\/doi.org\/10.5281\/zenodo.10040534 10.5281\/zenodo.10040534","DOI":"10.5281\/zenodo.10040534"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209153"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190315.1190324"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796810000079"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500599"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604150"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632866","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632866","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:02:51Z","timestamp":1751659371000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632866"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":38,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632866"],"URL":"https:\/\/doi.org\/10.1145\/3632866","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}