{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:20:53Z","timestamp":1750220453860,"version":"3.41.0"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2020,8,2]],"date-time":"2020-08-02T00:00:00Z","timestamp":1596326400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1524519"],"award-info":[{"award-number":["1524519"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000005","name":"U.S. Department of Defense","doi-asserted-by":"publisher","award":["FA9550-16-1-0082"],"award-info":[{"award-number":["FA9550-16-1-0082"]}],"id":[{"id":"10.13039\/100000005","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":[[2020,8,2]]},"abstract":"<jats:p>This paper describes an implementation of Harper's continuation-based regular-expression matcher as a strong functional program in Cedille; i.e., Cedille statically confirms termination of the program on all inputs. The approach uses neither dependent types nor termination proofs. Instead, a particular interface dubbed a recursion universe is provided by Cedille, and the language ensures that all programs written against this interface terminate. Standard polymorphic typing is all that is needed to check the code against the interface. This answers a challenge posed by Bove, Krauss, and Sozeau.<\/jats:p>","DOI":"10.1145\/3409004","type":"journal-article","created":{"date-parts":[[2020,8,3]],"date-time":"2020-08-03T13:48:02Z","timestamp":1596462482000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Strong functional pearl: Harper\u2019s regular-expression matcher in Cedille"],"prefix":"10.1145","volume":"4","author":[{"given":"Aaron","family":"Stump","sequence":"first","affiliation":[{"name":"University of Iowa, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5434-5018","authenticated-orcid":false,"given":"Christopher","family":"Jenkins","sequence":"additional","affiliation":[{"name":"University of Iowa, USA"}]},{"given":"Stephan","family":"Spahn","sequence":"additional","affiliation":[{"name":"University of Iowa, USA"}]},{"given":"Colin","family":"McDonald","sequence":"additional","affiliation":[{"name":"University of Notre Dame, USA"}]}],"member":"320","published-online":{"date-parts":[[2020,8,3]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1051\/ita:2007028"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034807"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_26"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129503004122"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000115"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00099-5"},{"key":"e_1_2_2_7_1","unstructured":"Robin Cockett. 1996. Charitable Thoughts. http:\/\/pll.cpsc.ucalgary.ca\/charity1\/www\/home. html (draft lecture notes).  Robin Cockett. 1996. Charitable Thoughts. http:\/\/pll.cpsc.ucalgary.ca\/charity1\/www\/home. html (draft lecture notes)."},{"key":"e_1_2_2_8_1","first-page":"183","volume-title":"Proceedings of the Symposium on Logic in Computer Science (LICS '87)","author":"Robert","year":"1987","unstructured":"Robert L. Constable and Scott F. Smith. 1987. Partial Objects In Constructive Type Theory . In Proceedings of the Symposium on Logic in Computer Science (LICS '87) , Ithaca, New York, USA , June 22-25, 1987 . IEEE Computer Society, 183 - 193 . Robert L. Constable and Scott F. Smith. 1987. Partial Objects In Constructive Type Theory. In Proceedings of the Symposium on Logic in Computer Science (LICS '87), Ithaca, New York, USA, June 22-25, 1987. IEEE Computer Society, 183-193."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11863-5_5"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863585"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.7146\/brics.v8i23.21684"},{"volume-title":"Eficient Mendler-Style Lambda-Encodings in Cedille","author":"Firsov Denis","key":"e_1_2_2_12_1","unstructured":"Denis Firsov , Richard Blair , and Aaron Stump . 2018. Eficient Mendler-Style Lambda-Encodings in Cedille . In Interactive Theorem Proving, Jeremy Avigad and Assia Mahboubi (Eds.). Springer International Publishing , Cham , 235-252. Denis Firsov, Richard Blair, and Aaron Stump. 2018. Eficient Mendler-Style Lambda-Encodings in Cedille. In Interactive Theorem Proving, Jeremy Avigad and Assia Mahboubi (Eds.). Springer International Publishing, Cham, 235-252."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9388-y"},{"volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Giesl J\u00fcrgen","key":"e_1_2_2_14_1","unstructured":"J\u00fcrgen Giesl , Albert Rubio , Christian Sternagel , Johannes Waldmann , and Akihisa Yamada . 2019. The Termination and Complexity Competition . In Tools and Algorithms for the Construction and Analysis of Systems , Dirk Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Stefen (Eds.). Springer International Publishing , Cham , 156-166. J\u00fcrgen Giesl, Albert Rubio, Christian Sternagel, Johannes Waldmann, and Akihisa Yamada. 2019. The Termination and Complexity Competition. In Tools and Algorithms for the Construction and Analysis of Systems, Dirk Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Stefen (Eds.). Springer International Publishing, Cham, 156-166."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003378"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2012.07.011"},{"volume-title":"Developments in Language Theory","author":"Holzer Markus","key":"e_1_2_2_17_1","unstructured":"Markus Holzer and Martin Kutrib . 2010. The Complexity of Regular(-Like) Expressions . In Developments in Language Theory , Yuan Gao, Hanlin Lu, Shinnosuke Seki, and Sheng Yu (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 16-30. Markus Holzer and Martin Kutrib. 2010. The Complexity of Regular(-Like) Expressions. In Developments in Language Theory, Yuan Gao, Hanlin Lu, Shinnosuke Seki, and Sheng Yu (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 16-30."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003500"},{"key":"e_1_2_2_19_1","volume-title":"Elaborating Inductive Datatypes and Course-of-Values Pattern Matching to Cedille. CoRR abs\/","author":"Jenkins Christopher","year":"1903","unstructured":"Christopher Jenkins , Colin McDonald , and Aaron Stump . 2019. Elaborating Inductive Datatypes and Course-of-Values Pattern Matching to Cedille. CoRR abs\/ 1903 .08233 ( 2019 ). arXiv: 1903.08233 http:\/\/arxiv.org\/abs\/ 1903.08233 Christopher Jenkins, Colin McDonald, and Aaron Stump. 2019. Elaborating Inductive Datatypes and Course-of-Values Pattern Matching to Cedille. CoRR abs\/ 1903.08233 ( 2019 ). arXiv: 1903.08233 http:\/\/arxiv.org\/abs\/ 1903.08233"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3310232.3310233"},{"key":"e_1_2_2_21_1","volume-title":"Monotone recursive types and recursive data representations in Cedille. arXiv:cs.PL\/","author":"Jenkins Christopher","year":"2001","unstructured":"Christopher Jenkins and Aaron Stump . 2020. Monotone recursive types and recursive data representations in Cedille. arXiv:cs.PL\/ 2001 .02828 Christopher Jenkins and Aaron Stump. 2020. Monotone recursive types and recursive data representations in Cedille. arXiv:cs.PL\/ 2001.02828"},{"key":"e_1_2_2_22_1","volume-title":"A Proof of the Standardization Theorem in \u03bb-Calculus. Lecture Notes: RIMS Kokyuroku Bessatsu 1217 (","author":"Kashima Ryo","year":"2001","unstructured":"Ryo Kashima . 2001. A Proof of the Standardization Theorem in \u03bb-Calculus. Lecture Notes: RIMS Kokyuroku Bessatsu 1217 ( June 2001 ). http:\/\/hdl.handle. net\/2433\/41230 Ryo Kashima. 2001. A Proof of the Standardization Theorem in \u03bb-Calculus. Lecture Notes: RIMS Kokyuroku Bessatsu 1217 ( June 2001 ). http:\/\/hdl.handle. net\/2433\/41230"},{"key":"e_1_2_2_23_1","unstructured":"Andrew Kent. 2017. Refinement Types in Typed Racket. https:\/\/blog.racket-lang.org\/ 2017 \/11\/adding-refinement-types.html  Andrew Kent. 2017. Refinement Types in Typed Racket. https:\/\/blog.racket-lang.org\/ 2017 \/11\/adding-refinement-types.html"},{"key":"e_1_2_2_24_1","unstructured":"Joomy Korkut Maksim Trifunovski and Daniel Licata. 2016. Intrinsic Verification of a Regular Expression Matcher. Unpublished available from Licata's web site.  Joomy Korkut Maksim Trifunovski and Daniel Licata. 2016. Intrinsic Verification of a Regular Expression Matcher. Unpublished available from Licata's web site."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9157-2"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578854.2503786"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211391"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/3540543961_7"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90069-X"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-008-9038-0"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52753-2_47"},{"volume-title":"Lectures on the Curry-Howard Isomorphism","author":"S\u00f8rensen Morten Heine","key":"e_1_2_2_33_1","unstructured":"Morten Heine S\u00f8rensen and Pawel Urzyczyn . 2006. Lectures on the Curry-Howard Isomorphism , Volume 149 ( Studies in Logic and the Foundations of Mathematics). Elsevier Science Inc . Morten Heine S\u00f8rensen and Pawel Urzyczyn. 2006. Lectures on the Curry-Howard Isomorphism, Volume 149 ( Studies in Logic and the Foundations of Mathematics). Elsevier Science Inc."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796817000053"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2018.03.002"},{"key":"e_1_2_2_36_1","volume-title":"Syntax and Semantics of Cedille. CoRR abs\/","author":"Stump Aaron","year":"1806","unstructured":"Aaron Stump . 2018b. Syntax and Semantics of Cedille. CoRR abs\/ 1806 .04709 ( 2018 ). arXiv: 1806.04709 http:\/\/arxiv.org\/abs\/ 1806.04709 Aaron Stump. 2018b. Syntax and Semantics of Cedille. CoRR abs\/ 1806.04709 ( 2018 ). arXiv: 1806.04709 http:\/\/arxiv.org\/abs\/ 1806.04709"},{"key":"e_1_2_2_37_1","volume-title":"Syntax and Typing for Cedille Core. CoRR abs\/","author":"Stump Aaron","year":"1811","unstructured":"Aaron Stump . 2018c. Syntax and Typing for Cedille Core. CoRR abs\/ 1811 .01318 ( 2018 ). arXiv: 1811.01318 http:\/\/arxiv.org\/ abs\/ 1811.01318 Aaron Stump. 2018c. Syntax and Typing for Cedille Core. CoRR abs\/ 1811.01318 ( 2018 ). arXiv: 1811.01318 http:\/\/arxiv.org\/ abs\/ 1811.01318"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"},{"key":"e_1_2_2_39_1","unstructured":"Alastair Telford and David Turner. 2000. Ensuring Termination in ESFP. 6 4 (apr 2000 ) 474-488. http:\/\/www.jucs.org\/jucs_6_4\/ensuring_termination_in_esfp.  Alastair Telford and David Turner. 2000. Ensuring Termination in ESFP. 6 4 (apr 2000 ) 474-488. http:\/\/www.jucs.org\/jucs_6_4\/ensuring_termination_in_esfp."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60675-0_35"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.3217\/jucs-010-07-0751"},{"key":"e_1_2_2_42_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 J. of Computing 6 , 3 (sep 1999 ), 343-361. http:\/\/dl.acm.org\/citation.cfm?id= 774455. 774462 Tarmo Uustalu and Varmo Vene. 1999. Mendler-style Inductive Types, Categorically. Nordic J. of Computing 6, 3 (sep 1999 ), 343-361. http:\/\/dl.acm.org\/citation.cfm?id= 774455. 774462","journal-title":"Nordic J. of Computing"},{"key":"e_1_2_2_43_1","volume-title":"Proc. of the 2nd Workshop on Generic Programming, WGP 2000","author":"Uustalu Tarmo","year":"2000","unstructured":"Tarmo Uustalu and Varmo Vene . 2000 . Coding Recursion a la Mendler (Extended Abstract) . In Proc. of the 2nd Workshop on Generic Programming, WGP 2000 , Technical Report UU-CS- 2000-19. Dept. of Computer Science, Utrecht University, 69-85. Tarmo Uustalu and Varmo Vene. 2000. Coding Recursion a la Mendler (Extended Abstract). In Proc. of the 2nd Workshop on Generic Programming, WGP 2000, Technical Report UU-CS-2000-19. Dept. of Computer Science, Utrecht University, 69-85."},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775050.2633366"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341705"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110275"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1019916231463"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3409004","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3409004","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3409004","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:59Z","timestamp":1750193279000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3409004"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,8,2]]},"references-count":46,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2020,8,2]]}},"alternative-id":["10.1145\/3409004"],"URL":"https:\/\/doi.org\/10.1145\/3409004","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2020,8,2]]},"assertion":[{"value":"2020-08-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}