{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:22:06Z","timestamp":1750220526591,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":42,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,8,18]],"date-time":"2021-08-18T00:00:00Z","timestamp":1629244800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Stiftelsen f\u00f6r Strategisk Forskning","award":["RIT17-0023"],"award-info":[{"award-number":["RIT17-0023"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,8,18]]},"DOI":"10.1145\/3471874.3472983","type":"proceedings-article","created":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T02:11:59Z","timestamp":1629339119000},"page":"56-70","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Practical normalization by evaluation for EDSLs"],"prefix":"10.1145","author":[{"given":"Nachiappan","family":"Valliappan","sequence":"first","affiliation":[{"name":"Chalmers University of Technology, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alejandro","family":"Russo","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sam","family":"Lindley","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,8,18]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3354166.3354168"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2013.09.007"},{"key":"e_1_3_2_1_3_1","volume-title":"Scott","author":"Altenkirch Thorsten","year":"2001","unstructured":"Thorsten Altenkirch , Peter Dybjer , Martin Hofmann , and Philip J . Scott . 2001 . Normalization by Evaluation for Typed Lambda Calculus with Coproducts. In LICS. IEEE Computer Society , 303\u2013310. Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, and Philip J. Scott. 2001. Normalization by Evaluation for Typed Lambda Calculus with Coproducts. In LICS. IEEE Computer Society, 303\u2013310."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2746325.2746334"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Robert Atkey Sam Lindley and Jeremy Yallop. 2009. Unembedding domain-specific languages. In Haskell. ACM 37\u201348.  Robert Atkey Sam Lindley and Jeremy Yallop. 2009. Unembedding domain-specific languages. In Haskell. ACM 37\u201348.","DOI":"10.1145\/1596638.1596644"},{"key":"e_1_3_2_1_6_1","volume-title":"IFL (Lecture Notes in Computer Science","volume":"136","author":"Axelsson Emil","year":"2010","unstructured":"Emil Axelsson , Koen Claessen , Mary Sheeran , Josef Svenningsson , David Engdal , and Anders Persson . 2010 . The Design and Implementation of Feldspar - An Embedded Language for Digital Signal Processing . In IFL (Lecture Notes in Computer Science , Vol. 6647). Springer, 121\u2013 136 . Emil Axelsson, Koen Claessen, Mary Sheeran, Josef Svenningsson, David Engdal, and Anders Persson. 2010. The Design and Implementation of Feldspar - An Embedded Language for Digital Signal Processing. In IFL (Lecture Notes in Computer Science, Vol. 6647). Springer, 121\u2013136."},{"key":"e_1_3_2_1_7_1","volume-title":"Roberto Di Cosmo, and Marcelo P. Fiore","author":"Balat Vincent","year":"2004","unstructured":"Vincent Balat , Roberto Di Cosmo, and Marcelo P. Fiore . 2004 . Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums. In POPL. ACM , 64\u201376. Vincent Balat, Roberto Di Cosmo, and Marcelo P. Fiore. 2004. Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums. In POPL. ACM, 64\u201376."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004099"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49254-2_4"},{"volume-title":"An Inverse of the Evaluation Functional for Typed lambda-calculus","author":"Berger Ulrich","key":"e_1_3_2_1_10_1","unstructured":"Ulrich Berger and Helmut Schwichtenberg . 1991. An Inverse of the Evaluation Functional for Typed lambda-calculus . In LICS. IEEE Computer Society , 203\u2013211. Ulrich Berger and Helmut Schwichtenberg. 1991. An Inverse of the Evaluation Functional for Typed lambda-calculus. In LICS. IEEE Computer Society, 203\u2013211."},{"key":"e_1_3_2_1_11_1","volume-title":"TYPES (Lecture Notes in Computer Science","volume":"61","author":"Beylin Ilya","year":"1995","unstructured":"Ilya Beylin and Peter Dybjer . 1995 . Extracting a Proof of Coherence for Monoidal Categories from a Proof of Normalization for Monoids . In TYPES (Lecture Notes in Computer Science , Vol. 1158). Springer, 47\u2013 61 . Ilya Beylin and Peter Dybjer. 1995. Extracting a Proof of Coherence for Monoidal Categories from a Proof of Normalization for Monoids. In TYPES (Lecture Notes in Computer Science, Vol. 1158). Springer, 47\u201361."},{"key":"e_1_3_2_1_12_1","volume-title":"Lava: Hardware Design in Haskell. In ICFP. ACM, 174\u2013184.","author":"Bjesse Per","year":"1998","unstructured":"Per Bjesse , Koen Claessen , Mary Sheeran , and Satnam Singh . 1998 . Lava: Hardware Design in Haskell. In ICFP. ACM, 174\u2013184. Per Bjesse, Koen Claessen, Mary Sheeran, and Satnam Singh. 1998. Lava: Hardware Design in Haskell. In ICFP. ACM, 174\u2013184."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809007205"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Manuel M. T. Chakravarty Gabriele Keller Sean Lee Trevor L. McDonell and Vinod Grover. 2011. Accelerating Haskell array codes with multicore GPUs. In DAMP. ACM 3\u201314.  Manuel M. T. Chakravarty Gabriele Keller Sean Lee Trevor L. McDonell and Vinod Grover. 2011. Accelerating Haskell array codes with multicore GPUs. In DAMP. ACM 3\u201314.","DOI":"10.1145\/1926354.1926358"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"James Cheney Sam Lindley and Philip Wadler. 2013. A practical theory of language-integrated query. In ICFP. ACM 403\u2013416.  James Cheney Sam Lindley and Philip Wadler. 2013. A practical theory of language-integrated query. In ICFP. ACM 403\u2013416.","DOI":"10.1145\/2544174.2500586"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0049326"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129596002150"},{"key":"e_1_3_2_1_18_1","volume-title":"Partial Evaluation (Lecture Notes in Computer Science","volume":"411","author":"Danvy Olivier","year":"1998","unstructured":"Olivier Danvy . 1998 . Type-Directed Partial Evaluation . In Partial Evaluation (Lecture Notes in Computer Science , Vol. 1706). Springer, 367\u2013 411 . Olivier Danvy. 1998. Type-Directed Partial Evaluation. In Partial Evaluation (Lecture Notes in Computer Science, Vol. 1706). Springer, 367\u2013411."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004166"},{"key":"e_1_3_2_1_20_1","volume-title":"APPSEM (Lecture Notes in Computer Science","volume":"192","author":"Dybjer Peter","year":"2000","unstructured":"Peter Dybjer and Andrzej Filinski . 2000 . Normalization and Partial Evaluation . In APPSEM (Lecture Notes in Computer Science , Vol. 2395). Springer, 137\u2013 192 . Peter Dybjer and Andrzej Filinski. 2000. Normalization and Partial Evaluation. In APPSEM (Lecture Notes in Computer Science, Vol. 2395). Springer, 137\u2013192."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/10704567_23"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_15"},{"key":"e_1_3_2_1_23_1","volume-title":"TLCA (Lecture Notes in Computer Science","volume":"185","author":"Ghani Neil","year":"1995","unstructured":"Neil Ghani . 1995 . \u03b2 \u03b7 -Equality for Coproducts . In TLCA (Lecture Notes in Computer Science , Vol. 902). Springer, 171\u2013 185 . Neil Ghani. 1995. \u03b2 \u03b7 -Equality for Coproducts. In TLCA (Lecture Notes in Computer Science, Vol. 902). Springer, 171\u2013185."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2605205"},{"key":"e_1_3_2_1_25_1","volume-title":"IFL (Lecture Notes in Computer Science","volume":"18","author":"Giorgidze George","year":"2010","unstructured":"George Giorgidze , Torsten Grust , Tom Schreiber , and Jeroen Weijers . 2010 . Haskell Boards the Ferry - Database-Supported Program Execution for Haskell . In IFL (Lecture Notes in Computer Science , Vol. 6647). Springer, 1\u2013 18 . George Giorgidze, Torsten Grust, Tom Schreiber, and Jeroen Weijers. 2010. Haskell Boards the Ferry - Database-Supported Program Execution for Haskell. In IFL (Lecture Notes in Computer Science, Vol. 6647). Springer, 1\u201318."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/242224.242477"},{"key":"e_1_3_2_1_27_1","volume-title":"Partial Evaluation and Automatic Program Generation","author":"Jones Neil D.","year":"2024","unstructured":"Neil D. Jones , Carsten K. Gomard , and Peter Sestoft . 1993. Partial Evaluation and Automatic Program Generation . Prentice-Hall, Inc. , USA. isbn:0130 2024 95 Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. 1993. Partial Evaluation and Automatic Program Generation. Prentice-Hall, Inc., USA. isbn:0130202495"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73228-0_19"},{"key":"e_1_3_2_1_30_1","volume-title":"NBE","author":"Lindley Sam","year":"2009","unstructured":"Sam Lindley . 2009 . Accumulating bindings . In NBE 2009. 49\u201356. Sam Lindley. 2009. Accumulating bindings. In NBE 2009. 49\u201356."},{"volume-title":"Logic Colloquium \u201973. 80","author":"Martin-L\u00f6f Per","key":"e_1_3_2_1_31_1","unstructured":"Per Martin-L\u00f6f . 1975. An Intuitionistic Theory of Types: Predicative Part . In Logic Colloquium \u201973. 80 , Elsevier , 73\u2013118. Per Martin-L\u00f6f. 1975. An Intuitionistic Theory of Types: Predicative Part. In Logic Colloquium \u201973. 80, Elsevier, 73\u2013118."},{"key":"e_1_3_2_1_32_1","volume-title":"Embedding by Normalisation. CoRR, abs\/1603.05197","author":"Najd Shayan","year":"2016","unstructured":"Shayan Najd , Sam Lindley , Josef Svenningsson , and Philip Wadler . 2016. Embedding by Normalisation. CoRR, abs\/1603.05197 ( 2016 ). Shayan Najd, Sam Lindley, Josef Svenningsson, and Philip Wadler. 2016. Embedding by Normalisation. CoRR, abs\/1603.05197 (2016)."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"crossref","unstructured":"Shayan Najd Sam Lindley Josef Svenningsson and Philip Wadler. 2016. Everything old is new again: quoted domain-specific languages. In PEPM. ACM 25\u201336.  Shayan Najd Sam Lindley Josef Svenningsson and Philip Wadler. 2016. Everything old is new again: quoted domain-specific languages. In PEPM. ACM 25\u201336.","DOI":"10.1145\/2847538.2847541"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"crossref","unstructured":"Frank Pfenning and Conal Elliott. 1988. Higher-Order Abstract Syntax. In PLDI. ACM 199\u2013208.  Frank Pfenning and Conal Elliott. 1988. Higher-Order Abstract Syntax. In PLDI. ACM 199\u2013208.","DOI":"10.1145\/960116.54010"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70849-8"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/641909.641910"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784760"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411286.1411289"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034675.2034688"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cl.2015.07.003"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2605685"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"crossref","unstructured":"Nachiappan Valliappan Robert Krook Alejandro Russo and Koen Claessen. 2020. Towards secure IoT programming in Haskell. In Haskell@ICFP. ACM 136\u2013150.  Nachiappan Valliappan Robert Krook Alejandro Russo and Koen Claessen. 2020. Towards secure IoT programming in Haskell. In Haskell@ICFP. ACM 136\u2013150.","DOI":"10.1145\/3406088.3409027"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236795"}],"event":{"name":"ICFP '21: 26th ACM SIGPLAN International Conference on Functional Programming","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Virtual Republic of Korea","acronym":"ICFP '21"},"container-title":["Proceedings of the 14th ACM SIGPLAN International Symposium on Haskell"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3471874.3472983","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3471874.3472983","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:24:49Z","timestamp":1750195489000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3471874.3472983"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,18]]},"references-count":42,"alternative-id":["10.1145\/3471874.3472983","10.1145\/3471874"],"URL":"https:\/\/doi.org\/10.1145\/3471874.3472983","relation":{},"subject":[],"published":{"date-parts":[[2021,8,18]]},"assertion":[{"value":"2021-08-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}