{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,20]],"date-time":"2025-10-20T18:35:24Z","timestamp":1760985324864,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,9,8]],"date-time":"2014-09-08T00:00:00Z","timestamp":1410134400000},"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":[[2014,9,8]]},"DOI":"10.1145\/2643135.2643146","type":"proceedings-article","created":{"date-parts":[[2015,7,6]],"date-time":"2015-07-06T14:04:29Z","timestamp":1436191469000},"page":"57-68","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["A Type Theoretic Specification of Partial Evaluation"],"prefix":"10.1145","author":[{"given":"Kenichi","family":"Asai","sequence":"first","affiliation":[{"name":"Ochanomizu University, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luminous","family":"Fennell","sequence":"additional","affiliation":[{"name":"University of Freiburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Thiemann","sequence":"additional","affiliation":[{"name":"University of Freiburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yang","family":"Zhang","sequence":"additional","affiliation":[{"name":"University of Freiburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,9,8]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_3_2_1_1_1","DOI":"10.1145\/1146809.1146812"},{"unstructured":"K.\n       \n      Asai\n    .\n      \n  \n   \n  Logical relations for call-by-value delimited continuations. In M. C. J. D. van Eekelen editor TFP\n   \n  2005 volume \n  6\n   of \n  Trends in Functional Programming pages \n  63\n  --\n  78 Tallinn Estonia 2005. Intellect. \n  ISBN\n   978-1-84150-176-5.  K. Asai. Logical relations for call-by-value delimited continuations. In M. C. J. D. van Eekelen editor TFP 2005 volume 6 of Trends in Functional Programming pages 63--78 Tallinn Estonia 2005. Intellect. ISBN 978-1-84150-176-5.","key":"e_1_3_2_1_2_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_3_1","DOI":"10.1007\/978-3-642-03359-9_6"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_4_1","DOI":"10.1023\/A:1019964114625"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_5_1","DOI":"10.1145\/237721.237784"},{"volume-title":"Proc. Third Fuji International Symposium on Functional and Logic Programming","year":"1998","author":"Danvy O.","key":"e_1_3_2_1_6_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_7_1","DOI":"10.1017\/S0960129500001535"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_8_1","DOI":"10.1007\/BF01019004"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_9_1","DOI":"10.5555\/788018.788825"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_10_1","DOI":"10.1145\/237721.237788"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_11_1","DOI":"10.1016\/1385-7258(72)90034-0"},{"doi-asserted-by":"crossref","unstructured":"D.\n       \n      Dussart F.\n       \n      Henglein and \n      \n      \n      C.\n       \n      Mossin\n      \n  \n  . \n  Polymorphic recursion and subtype qualifications: Polymorphic binding-time analysis in polynomial time. In A. Mycroft editor Proc. 1995 International Static Analysis Symposium volume \n  983\n   of \n  LNCS pages \n  118\n  --\n  136 Glasgow Scotland Sept\n  . \n  1995\n  . \n  Springer\n  . URL ftp:\/\/ftp.diku.dk\/diku\/semantics\/papers\/D-243.dvi.gz.   D. Dussart F. Henglein and C. Mossin. Polymorphic recursion and subtype qualifications: Polymorphic binding-time analysis in polynomial time. In A. Mycroft editor Proc. 1995 International Static Analysis Symposium volume 983 of LNCS pages 118--136 Glasgow Scotland Sept. 1995. Springer. URL ftp:\/\/ftp.diku.dk\/diku\/semantics\/papers\/D-243.dvi.gz.","key":"e_1_3_2_1_12_1","DOI":"10.1007\/3-540-60360-3_36"},{"unstructured":"A.\n       \n      Filinski\n    .\n      \n  \n   \n  A semantic account of type-directed partial evaluation. In G. Nadathur editor PPDP volume \n  1702\n   of \n  Lecture Notes in Computer Science pages \n  378\n  --\n  395 Paris France Sept\n  . \n  1999\n  . \n  Springer\n  . ISBN 3-540-66540-4.   A. Filinski. A semantic account of type-directed partial evaluation. In G. Nadathur editor PPDP volume 1702 of Lecture Notes in Computer Science pages 378--395 Paris France Sept. 1999. Springer. ISBN 3-540-66540-4.","key":"e_1_3_2_1_13_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_14_1","DOI":"10.1017\/S0956796800000058"},{"unstructured":"J.\n       \n      Hatcliff\n    .\n      \n  \n   \n  Mechanically verifying the correctness of an offline partial evaluator. In S. D. Swierstra and M. Hermenegildo editors PLILP '95 volume \n  982\n   of \n  LNCS pages \n  279\n  --\n  298 Utrecht The Netherlands Sept. \n  1995\n  . \n  Springer\n  . ISBN 3-540-60359-X.   J. Hatcliff. Mechanically verifying the correctness of an offline partial evaluator. In S. D. Swierstra and M. Hermenegildo editors PLILP '95 volume 982 of LNCS pages 279--298 Utrecht The Netherlands Sept. 1995. Springer. ISBN 3-540-60359-X.","key":"e_1_3_2_1_15_1"},{"doi-asserted-by":"crossref","unstructured":"J.\n       \n      Hatcliff T.\n       \u00c6. \n      Mogensen and \n      \n      \n      P.\n       \n      Thiemann editors\n      \n  \n  . \n  Partial Evaluation---Practice and Theory. Proceedings of the 1998 DIKU International Summerschool volume \n  1706\n   of \n  LNCS Copenhagen Denmark 1999\n  . \n  Springer\n  .  J. Hatcliff T. \u00c6. Mogensen and P. Thiemann editors. Partial Evaluation---Practice and Theory. Proceedings of the 1998 DIKU International Summerschool volume 1706 of LNCS Copenhagen Denmark 1999. Springer.","key":"e_1_3_2_1_16_1","DOI":"10.1007\/3-540-47018-2"},{"key":"e_1_3_2_1_17_1","series-title":"LNCS","first-page":"287","volume-title":"5th ESOP","author":"Henglein F.","year":"1994"},{"volume-title":"Prentice-Hall, 1993","year":"2024","author":"Jones N.","key":"e_1_3_2_1_18_1"},{"volume-title":"University of Copenhagen","year":"1991","author":"J\u00f8rgensen J.","key":"e_1_3_2_1_19_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_20_1","DOI":"10.1016\/j.ic.2010.09.008"},{"volume-title":"Bibliopolis","year":"1984","author":"Martin-L\u00f6f P.","key":"e_1_3_2_1_21_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_22_1","DOI":"10.1016\/0168-0072(91)90067-V"},{"doi-asserted-by":"crossref","unstructured":"F.\n       \n      Nielson\n     and \n      \n      \n      H. R.\n       \n      Nielson\n      \n  \n  . \n  Two-Level Functional Languages volume \n  34\n   of \n  Cambridge Tracts in Theoretical Computer Science\n  . \n  Cambridge University Press 1992\n  .   F. Nielson and H. R. Nielson. Two-Level Functional Languages volume 34 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press 1992.","key":"e_1_3_2_1_23_1","DOI":"10.1017\/CBO9780511526572"},{"unstructured":"U.\n       \n      Norell\n    .\n      \n  \n   \n  Dependently typed programming in Agda. In P. W. M. Koopman R. Plasmeijer and S. D. Swierstra editors Advanced Functional Programming volume \n  5832\n   of \n  LNCS pages \n  230\n  --\n  266 Heijen The Netherlands 2008\n  . \n  Springer\n  . ISBN 978-3-642-04651-3.   U. Norell. Dependently typed programming in Agda. In P. W. M. Koopman R. Plasmeijer and S. D. Swierstra editors Advanced Functional Programming volume 5832 of LNCS pages 230--266 Heijen The Netherlands 2008. Springer. ISBN 978-3-642-04651-3.","key":"e_1_3_2_1_24_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_25_1","DOI":"10.5555\/120477.120483"},{"unstructured":"B. C. Pierce etal Software foundations. http:\/\/www.cis.upenn.edu\/~bcpierce\/sf\/ July 2013.  B. C. Pierce et al. Software foundations. http:\/\/www.cis.upenn.edu\/~bcpierce\/sf\/ July 2013.","key":"e_1_3_2_1_26_1"},{"key":"e_1_3_2_1_27_1","first-page":"769","volume-title":"Proc. 1996 ACM Symp. POPL, St","author":"POPL","year":"1996"},{"volume-title":"Oregon Graduate Institute of Science and Technology","year":"1999","author":"Taha W.","key":"e_1_3_2_1_28_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_29_1","DOI":"10.1145\/604131.604134"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_30_1","DOI":"10.1017\/S0956796800000782"}],"event":{"sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"acronym":"PPDP '14","name":"PPDP '14: 16th International Symposium on Principles and Practice of Declarative Programming","location":"Canterbury United Kingdom"},"container-title":["Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2643135.2643146","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2643135.2643146","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:01:01Z","timestamp":1750230061000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2643135.2643146"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,9,8]]},"references-count":30,"alternative-id":["10.1145\/2643135.2643146","10.1145\/2643135"],"URL":"https:\/\/doi.org\/10.1145\/2643135.2643146","relation":{},"subject":[],"published":{"date-parts":[[2014,9,8]]},"assertion":[{"value":"2014-09-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}