{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T18:14:03Z","timestamp":1781892843878,"version":"3.54.5"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,1,2]],"date-time":"2017-01-02T00:00:00Z","timestamp":1483315200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,1,2]]},"DOI":"10.1145\/3018882.3020004","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T21:20:29Z","timestamp":1482441629000},"page":"1-11","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Compiling untyped lambda calculus to lower-level code by game semantics and partial evaluation (invited paper)"],"prefix":"10.1145","author":[{"given":"Daniil","family":"Berezun","sequence":"first","affiliation":[{"name":"JetBrains, Russia \/ St. Petersburg State University, Russia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Neil D.","family":"Jones","sequence":"additional","affiliation":[{"name":"University of Copenhagen, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,1,2]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1044"},{"key":"e_1_3_2_1_3_1","first-page":"115","volume-title":"International Conference TACS 94","author":"Abramsky Samson","year":"1994","unstructured":"Samson Abramsky , Pasquale Malacaria , and Radha Jagadeesan . Full abstraction for PCF. In Theoretical Aspects of Computer Software , International Conference TACS 94 , pages 115 , 1994 . Samson Abramsky, Pasquale Malacaria, and Radha Jagadeesan. Full abstraction for PCF. In Theoretical Aspects of Computer Software, International Conference TACS 94, pages 115, 1994."},{"key":"e_1_3_2_1_4_1","first-page":"156","volume-title":"Computational Logic: Proceedings of the 1997 Marktoberdorf Summer School","author":"Abramsky S.","unstructured":"S. Abramsky and G. McCusker . Game semantics . In Computational Logic: Proceedings of the 1997 Marktoberdorf Summer School , pages 156 . Springer Verlag, 1999. S. Abramsky and G. McCusker. Game semantics. In Computational Logic: Proceedings of the 1997 Marktoberdorf Summer School, pages 156. Springer Verlag, 1999."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2917"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/539640"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"David A.\n      Schmidt\n    .\n  State transition machines for lambda calculus expressions\n  . In Neil D. Jones editor Semantics-Directed Compiler Generation volume \n  94\n   of \n  Lecture Notes in Computer Science pages \n  415440\n  . Springer 1980.   David A. Schmidt. State transition machines for lambda calculus expressions. In Neil D. Jones editor Semantics-Directed Compiler Generation volume 94 of Lecture Notes in Computer Science pages 415440. Springer 1980.","DOI":"10.1007\/3-540-10250-7_32"},{"key":"e_1_3_2_1_8_1","volume-title":"Normalisation by traversals. CoRR, abs\/1511.02629","author":"Luke Ong C.-H.","year":"2015","unstructured":"C.-H. Luke Ong . Normalisation by traversals. CoRR, abs\/1511.02629 , 2015 . C.-H. Luke Ong. Normalisation by traversals. CoRR, abs\/1511.02629, 2015."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.38"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364578"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00353-4"},{"key":"e_1_3_2_1_12_1","volume-title":"Head linear reduction. unpublished","author":"Danos Vincent","year":"2004","unstructured":"Vincent Danos and Laurent Regnier . Head linear reduction. unpublished , 2004 . Vincent Danos and Laurent Regnier. Head linear reduction. unpublished, 2004."},{"key":"e_1_3_2_1_13_1","volume-title":"The lambda calculus : its syntax and semantics. Studies in logic and the foundations of mathematics. North-Holland","author":"Barendregt Hendrik Pieter","year":"1981","unstructured":"Hendrik Pieter Barendregt . The lambda calculus : its syntax and semantics. Studies in logic and the foundations of mathematics. North-Holland , Amsterdam , New-York, Oxford , 1981 . Hendrik Pieter Barendregt. The lambda calculus : its syntax and semantics. Studies in logic and the foundations of mathematics. North-Holland, Amsterdam, New-York, Oxford, 1981."},{"key":"e_1_3_2_1_14_1","series-title":"Lecture Notes in Computer Science","first-page":"420435","volume-title":"The Essence of Computation, Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones {on occasion of his 60th birthday}","author":"Sestoft Peter","unstructured":"Peter Sestoft . Demonstrating lambda calculus reduction . In Torben. Mogensen, David A. Schmidt, and Ivan Hal Sudborough, editors, The Essence of Computation, Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones {on occasion of his 60th birthday} , volume 2566 of Lecture Notes in Computer Science , pages 420435 . Springer, 2002. Peter Sestoft. Demonstrating lambda calculus reduction. In Torben. Mogensen, David A. Schmidt, and Ivan Hal Sudborough, editors, The Essence of Computation, Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones {on occasion of his 60th birthday}, volume 2566 of Lecture Notes in Computer Science, pages 420435. Springer, 2002."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.03.010"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010027404223"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/262244"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/153676"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.34"},{"key":"e_1_3_2_1_20_1","first-page":"445463","volume-title":"Partial Evaluation and Mixed Computation","author":"Romanenko S.A.","unstructured":"S.A. Romanenko . A compiler generator produced by a self-applicable specializer can have a surprisingly natural and understandable structure . In Dines Bjrner, Andrei Ershov, and Neil D. Jones, editors, Partial Evaluation and Mixed Computation , pages 445463 . North Holland, 1988. S.A. Romanenko. A compiler generator produced by a self-applicable specializer can have a surprisingly natural and understandable structure. In Dines Bjrner, Andrei Ershov, and Neil D. Jones, editors, Partial Evaluation and Mixed Computation, pages 445463. North Holland, 1988."},{"key":"e_1_3_2_1_21_1","volume-title":"6th International Symposium, PLILP94","author":"Birkedal L.","year":"1994","unstructured":"L. Birkedal and M. Welinder . Hand-writing program generator generators. In M.V. Hermenegildo and J. Penjam, editors, Programming Language Implementation and Logic Programming , 6th International Symposium, PLILP94 , Madrid, Spain , September , 1994 . (Lecture Notes in Computer Science, Vol. 844), pages 198214. Springer-Verlag, 1994. L. Birkedal and M. Welinder. Hand-writing program generator generators. In M.V. Hermenegildo and J. Penjam, editors, Programming Language Implementation and Logic Programming, 6th International Symposium, PLILP94, Madrid, Spain, September, 1994. (Lecture Notes in Computer Science, Vol. 844), pages 198214. Springer-Verlag, 1994."},{"key":"e_1_3_2_1_22_1","volume-title":"UNP: strong normalisation of the untyped -expression by linear head reduction. ongoing work","author":"Berezun Daniil","year":"2016","unstructured":"Daniil Berezun . UNP: strong normalisation of the untyped -expression by linear head reduction. ongoing work , 2016 . Daniil Berezun. UNP: strong normalisation of the untyped -expression by linear head reduction. ongoing work, 2016."},{"key":"e_1_3_2_1_24_1","volume-title":"The Implementation of Functional Programming Languages","author":"Peyton Jones Simon L.","year":"1987","unstructured":"Simon L. Peyton Jones . The Implementation of Functional Programming Languages . Prentice-Hall , 1987 . Simon L. Peyton Jones. The Implementation of Functional Programming Languages. Prentice-Hall, 1987."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.03.058"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158618"},{"key":"e_1_3_2_1_27_1","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Caclulus and Formalism","author":"L\u00e9vy Jean-Jacques","year":"1980","unstructured":"Jean-Jacques L\u00e9vy . Optimal reductions in the lambda-calculus . In To H.B. Curry: Essays on Combinatory Logic, Lambda Caclulus and Formalism . Academic Press , 1980 . Jean-Jacques L\u00e9vy. Optimal reductions in the lambda-calculus. In To H.B. Curry: Essays on Combinatory Logic, Lambda Caclulus and Formalism. Academic Press, 1980."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96711"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_16"},{"key":"e_1_3_2_1_30_1","volume-title":"Workshop on Algebra and Logic on Programming Systems (ALPS)","author":"de Looij Kees-Lan","year":"2004","unstructured":"Kees-Lan can de Looij Vincent van Oostrom and Mariln Zwitserlood . Lambdascope another optimal implementation of the lambda-calculus . In Workshop on Algebra and Logic on Programming Systems (ALPS) , 2004 . Kees-Lan can de Looij Vincent van Oostrom and Mariln Zwitserlood. Lambdascope another optimal implementation of the lambda-calculus. In Workshop on Algebra and Logic on Programming Systems (ALPS), 2004."},{"key":"e_1_3_2_1_31_1","first-page":"381392","article-title":"Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem","volume":"34","author":"De Bruijn N. G.","year":"1972","unstructured":"N. G. De Bruijn . Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem . INDAG. MATH , 34 : 381392 , 1972 . N. G. De Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. INDAG. MATH, 34:381392, 1972.","journal-title":"INDAG. MATH"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96718"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/232627.232639"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/860256"},{"key":"e_1_3_2_1_35_1","volume-title":"Galop 2008:Games for Logic and Programming Languages","author":"Blum William","year":"2008","unstructured":"William Blum and C.-H. Luke Ong . A concrete presentation of game semantics . In Galop 2008:Games for Logic and Programming Languages , 2008 . William Blum and C.-H. Luke Ong. A concrete presentation of game semantics. In Galop 2008:Games for Logic and Programming Languages, 2008."},{"key":"e_1_3_2_1_36_1","volume-title":"The safe lambda calculus. Logic Methods in Computer Science, 5(1)","author":"Blum William","year":"2009","unstructured":"William Blum and C.-H. Luke Ong . The safe lambda calculus. Logic Methods in Computer Science, 5(1) , 2009 . William Blum and C.-H. Luke Ong. The safe lambda calculus. Logic Methods in Computer Science, 5(1), 2009."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1993.287578"}],"event":{"name":"POPL '17: The 44th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","location":"Paris France","acronym":"POPL '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3018882.3020004","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3018882.3020004","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:24:12Z","timestamp":1750220652000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3018882.3020004"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1,2]]},"references-count":36,"alternative-id":["10.1145\/3018882.3020004","10.1145\/3018882"],"URL":"https:\/\/doi.org\/10.1145\/3018882.3020004","relation":{},"subject":[],"published":{"date-parts":[[2017,1,2]]},"assertion":[{"value":"2017-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}