{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:19:27Z","timestamp":1750220367779,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":29,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,9,2]],"date-time":"2020-09-02T00:00:00Z","timestamp":1599004800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-16-1-0082"],"award-info":[{"award-number":["FA9550-16-1-0082"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,9,2]]},"DOI":"10.1145\/3462172.3462194","type":"proceedings-article","created":{"date-parts":[[2021,7,23]],"date-time":"2021-07-23T22:06:52Z","timestamp":1627078012000},"page":"93-103","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Zero-Cost Constructor Subtyping"],"prefix":"10.1145","author":[{"given":"Andrew","family":"Marmaduke","sequence":"first","affiliation":[{"name":"The University of Iowa, Computer Science, Iowa City, IA, United States"}]},{"given":"Christopher","family":"Jenkins","sequence":"additional","affiliation":[{"name":"The University of Iowa, Computer Science, Iowa City, IA, United States"}]},{"given":"Aaron","family":"Stump","sequence":"additional","affiliation":[{"name":"The University of Iowa, Computer Science, Iowa City, IA, United States"}]}],"member":"320","published-online":{"date-parts":[[2021,7,23]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.10.017"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2005.10.005"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49099-X_8"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46432-8_2"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1069774.1069793"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1033"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-3452-7_18"},{"key":"e_1_3_2_1_8_1","volume-title":"Informal proceedings of Logical Frameworks, Vol.\u00a092","author":"Coquand Thierry","year":"1992","unstructured":"Thierry Coquand . 1992 . Pattern matching with dependent types . In Informal proceedings of Logical Frameworks, Vol.\u00a092 . Citeseer, 66\u201379. Thierry Coquand. 1992. Pattern matching with dependent types. In Informal proceedings of Logical Frameworks, Vol.\u00a092. Citeseer, 66\u201379."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236799"},{"volume-title":"Algebraic subtyping. BCS","author":"Dolan Stephen","key":"e_1_3_2_1_10_1","unstructured":"Stephen Dolan . 2017. Algebraic subtyping. BCS , The Chartered Institute for IT. Stephen Dolan. 2017. Algebraic subtyping. BCS, The Chartered Institute for IT."},{"key":"e_1_3_2_1_11_1","volume-title":"Efficient Mendler-Style Lambda-Encodings in Cedille. In International Conference on Interactive Theorem Proving. Springer, 235\u2013252","author":"Firsov Denis","year":"2018","unstructured":"Denis Firsov , Richard Blair , and Aaron Stump . 2018 . Efficient Mendler-Style Lambda-Encodings in Cedille. In International Conference on Interactive Theorem Proving. Springer, 235\u2013252 . Denis Firsov, Richard Blair, and Aaron Stump. 2018. Efficient Mendler-Style Lambda-Encodings in Cedille. In International Conference on Interactive Theorem Proving. Springer, 235\u2013252."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664588"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1391289.1391293"},{"key":"e_1_3_2_1_14_1","volume-title":"Induction Is Not Derivable in Second Order Dependent Type Theory. In International Conference on Typed Lambda Calculi and Applications, Samson Abramsky (Ed.). Springer","author":"Geuvers Herman","year":"2001","unstructured":"Herman Geuvers . 2001 . Induction Is Not Derivable in Second Order Dependent Type Theory. In International Conference on Typed Lambda Calculi and Applications, Samson Abramsky (Ed.). Springer , Berlin, Heidelberg, 166\u2013181. Herman Geuvers. 2001. Induction Is Not Derivable in Second Order Dependent Type Theory. In International Conference on Typed Lambda Calculi and Applications, Samson Abramsky (Ed.). Springer, Berlin, Heidelberg, 166\u2013181."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(02)00025-4"},{"key":"e_1_3_2_1_16_1","unstructured":"Christopher Jenkins and Aaron Stump. 2020. Monotone recursive types and recursive data representations in Cedille. arxiv:2001.02828\u00a0[cs.PL] Under consideration for publication in J. Mathematically Structured Computer Science.  Christopher Jenkins and Aaron Stump. 2020. Monotone recursive types and recursive data representations in Cedille. arxiv:2001.02828\u00a0[cs.PL] Under consideration for publication in J. Mathematically Structured Computer Science."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2003.1210048"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01110627"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/9.1.105"},{"key":"e_1_3_2_1_20_1","volume-title":"12th International Workshop, CSL \u201998, Annual Conference of the EACSL, Brno, Czech Republic, August 24-28, 1998, Proceedings(Lecture Notes in Computer Science, Vol.\u00a01584)","author":"Matthes Ralph","year":"1998","unstructured":"Ralph Matthes . 1998 . Monotone Fixed-Point Types and Strong Normalization. In Computer Science Logic , 12th International Workshop, CSL \u201998, Annual Conference of the EACSL, Brno, Czech Republic, August 24-28, 1998, Proceedings(Lecture Notes in Computer Science, Vol.\u00a01584) , Georg Gottlob, Etienne Grandjean, and Katrin Seyr (Eds.). Springer, 298\u2013312. https:\/\/doi.org\/10.1007\/10703163_20 10.1007\/10703163_20 Ralph Matthes. 1998. Monotone Fixed-Point Types and Strong Normalization. In Computer Science Logic, 12th International Workshop, CSL \u201998, Annual Conference of the EACSL, Brno, Czech Republic, August 24-28, 1998, Proceedings(Lecture Notes in Computer Science, Vol.\u00a01584), Georg Gottlob, Etienne Grandjean, and Katrin Seyr (Eds.). Springer, 298\u2013312. https:\/\/doi.org\/10.1007\/10703163_20"},{"key":"e_1_3_2_1_21_1","volume-title":"Proceedings of the Symposium on Logic in Computer Science((LICS \u201987)","author":"Mendler P.","year":"1987","unstructured":"N.\u00a0 P. Mendler . 1987 . Recursive Types and Type Constraints in Second-Order Lambda Calculus . In Proceedings of the Symposium on Logic in Computer Science((LICS \u201987) ). IEEE Computer Society, Los Alamitos, CA, 30\u201336. N.\u00a0P. Mendler. 1987. Recursive Types and Type Constraints in Second-Order Lambda Calculus. In Proceedings of the Symposium on Logic in Computer Science((LICS \u201987)). IEEE Computer Society, Los Alamitos, CA, 30\u201336."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90069-X"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_27"},{"key":"e_1_3_2_1_24_1","volume-title":"10th International Conference on Interactive Theorem Proving (ITP","author":"Ringer Talia","year":"2019","unstructured":"Talia Ringer , Nathaniel Yazdani , John Leo , and Dan Grossman . 2019 . Ornaments for proof reuse in Coq . In 10th International Conference on Interactive Theorem Proving (ITP 2019). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. 2019. Ornaments for proof reuse in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96746"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796817000053"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2018.03.002"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"},{"key":"e_1_3_2_1_29_1","first-page":"3","article-title":"Mendler-style Inductive Types, Categorically","volume":"6","author":"Uustalu Tarmo","year":"1999","unstructured":"Tarmo Uustalu and Varmo Vene . 1999 . Mendler-style Inductive Types, Categorically . Nordic Journal of Computing 6 , 3 (Sep 1999), 343\u2013361. http:\/\/dl.acm.org\/citation.cfm?id=774455.774462 Tarmo Uustalu and Varmo Vene. 1999. Mendler-style Inductive Types, Categorically. Nordic Journal of Computing 6, 3 (Sep 1999), 343\u2013361. http:\/\/dl.acm.org\/citation.cfm?id=774455.774462","journal-title":"Nordic Journal of Computing"}],"event":{"name":"IFL 2020: 32nd Symposium on Implementation and Application of Functional Languages","acronym":"IFL 2020","location":"Canterbury United Kingdom"},"container-title":["Proceedings of the 32nd Symposium on Implementation and Application of Functional Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3462172.3462194","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3462172.3462194","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3462172.3462194","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:17:34Z","timestamp":1750191454000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3462172.3462194"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9,2]]},"references-count":29,"alternative-id":["10.1145\/3462172.3462194","10.1145\/3462172"],"URL":"https:\/\/doi.org\/10.1145\/3462172.3462194","relation":{},"subject":[],"published":{"date-parts":[[2020,9,2]]},"assertion":[{"value":"2021-07-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}