{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:53:11Z","timestamp":1740099191108,"version":"3.37.3"},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030027674"},{"type":"electronic","value":"9783030027681"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-02768-1_20","type":"book-chapter","created":{"date-parts":[[2018,10,21]],"date-time":"2018-10-21T07:42:27Z","timestamp":1540107747000},"page":"375-393","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Certifying CPS Transformation of Let-Polymorphic Calculus Using PHOAS"],"prefix":"10.1007","author":[{"given":"Urara","family":"Yamada","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kenichi","family":"Asai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,10,22]]},"reference":[{"key":"20_CR1","volume-title":"Compiling with Continuations","author":"AW Appel","year":"2007","unstructured":"Appel, A.W.: Compiling with Continuations. Cambridge University Press, New York (2007)"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-76637-7_16","volume-title":"Programming Languages and Systems","author":"K Asai","year":"2007","unstructured":"Asai, K., Kameyama, Y.: Polymorphic delimited continuations. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 239\u2013254. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-76637-7_16"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Asai, K., Uehara, C.: Selective CPS transformation for shift and reset. In: Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2018), pp. 40\u201352 (2018)","DOI":"10.1145\/3162069"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/11541868_4","volume-title":"Theorem Proving in Higher Order Logics","author":"BE Aydemir","year":"2005","unstructured":"Aydemir, B.E., et al.: Mechanized metatheory for the masses: the PoplMark challenge. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 50\u201365. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11541868_4"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"de Bruijn, N.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. In: Indagationes Mathematicae, Proceedings, vol. 75, no. 5, pp. 381\u2013392 (1972)","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Parametric higher-order abstract syntax for mechanized semantics. In: Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP 2008), pp. 143\u2013156, September 2008","DOI":"10.1145\/1411204.1411226"},{"key":"20_CR7","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/9153.001.0001","volume-title":"Certified Programming with Dependent Types","author":"A Chlipala","year":"2013","unstructured":"Chlipala, A.: Certified Programming with Dependent Types. MIT Press, Cambridge (2013)"},{"key":"20_CR8","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0167-6423(94)00003-4","volume":"22","author":"O Danvy","year":"1994","unstructured":"Danvy, O.: Back to Direct Style. Sci. Comput. Program. 22, 183\u2013195 (1994)","journal-title":"Sci. Comput. Program."},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Danvy, O., Filinski, A.: Abstracting control. In: Proceedings of the ACM Conference on LISP and Functional Programming (LFP 1990), pp. 151\u2013160 (1990)","DOI":"10.1145\/91556.91622"},{"issue":"4","key":"20_CR10","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1017\/S0960129500001535","volume":"2","author":"O Danvy","year":"1992","unstructured":"Danvy, O., Filinski, A.: Representing control: a study of the CPS transformation. Math. Struct. Comput. Sci. 2(4), 361\u2013391 (1992)","journal-title":"Math. Struct. Comput. Sci."},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Dargaye, Z., Leroy, X.: Mechanized verification of CPS transformations. In: Proceedings of the International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2005), pp. 211\u2013225 (2007)","DOI":"10.1007\/978-3-540-75560-9_17"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Minamide, Y., Okuma, K.: Verifying CPS transformations in Isabelle\/HOL. In: Proceedings of the 2003 ACM SIGPLAN Workshop on Mechanized Reasoning About Languages with Variable Binding (MERLIN 2003), pp. 1\u20138 (2003)","DOI":"10.1145\/976571.976576"},{"key":"20_CR13","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1016\/S1571-0661(04)80969-1","volume":"45","author":"LR Nielsen","year":"2001","unstructured":"Nielsen, L.R.: A selective CPS transformation. Electron. Notes Theor. Comput. Sci. 45, 311\u2013331 (2001)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"20_CR14","volume-title":"Types and Programming Languages","author":"BC Pierce","year":"2002","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)"},{"key":"20_CR15","unstructured":"Tian, Y.H.: Mechanically verifying correctness of CPS compilation. In: Proceeding of the Twelfth Computing: The Australasian Theory Symposium (CATS 2006), vol. 51, pp. 41\u201351 (2006)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-02768-1_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,27]],"date-time":"2019-10-27T06:11:33Z","timestamp":1572156693000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-02768-1_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030027674","9783030027681"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-02768-1_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Wellington","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New Zealand","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 December 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 December 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/aplas2018.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}