{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:08:29Z","timestamp":1750219709016,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":18,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,10,22]],"date-time":"2023-10-22T00:00:00Z","timestamp":1697932800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"EPSRC","award":["EP\/T008911\/1"],"award-info":[{"award-number":["EP\/T008911\/1"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,10,22]]},"DOI":"10.1145\/3610612.3610613","type":"proceedings-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T23:13:48Z","timestamp":1697498028000},"page":"1-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A Calculus of Delayed Reductions"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2077-011X","authenticated-orcid":false,"given":"Steffen","family":"Van Bakel","sequence":"first","affiliation":[{"name":"Computing, Imperial College London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4161-985X","authenticated-orcid":false,"given":"Nicolas","family":"Wu","sequence":"additional","affiliation":[{"name":"Computing, Imperial College London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-2849-0443","authenticated-orcid":false,"given":"Emma","family":"Tye","sequence":"additional","affiliation":[{"name":"Computing, Imperial College London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,10,22]]},"reference":[{"volume-title":"The Lambda Calculus: its Syntax and Semantics (revised ed.). North-Holland","author":"Barendregt H.","key":"e_1_3_2_1_1_1","unstructured":"H. Barendregt . 1984. The Lambda Calculus: its Syntax and Semantics (revised ed.). North-Holland , Amsterdam . https:\/\/doi.org\/10.2307\/2274112 10.2307\/2274112 H. Barendregt. 1984. The Lambda Calculus: its Syntax and Semantics (revised ed.). North-Holland, Amsterdam. https:\/\/doi.org\/10.2307\/2274112"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1936-1501858-0"},{"volume-title":"Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming (ICFP\u201900)","author":"Curien P.-L.","key":"e_1_3_2_1_3_1","unstructured":"P.-L. Curien and H. Herbelin . 2000. The Duality of Computation . In Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming (ICFP\u201900) (ACM Sigplan Notices), Vol.\u00a035.9. ACM, 233\u2013243. https:\/\/doi.org\/10.1145\/351240.351262 10.1145\/351240.351262 P.-L. Curien and H. Herbelin. 2000. The Duality of Computation. In Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming (ICFP\u201900)(ACM Sigplan Notices), Vol.\u00a035.9. ACM, 233\u2013243. https:\/\/doi.org\/10.1145\/351240.351262"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.2307\/2370619"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_9"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2967973.2968608"},{"volume-title":"Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs. Association for Computing Machinery","author":"Forster Y.","key":"e_1_3_2_1_7_1","unstructured":"Y. Forster , S. Sch\u00e4fer , S. Spies , and K. Stark . 2019. Call-by-Push-Value in Coq: Operational, Equational, and Denotational Theory . In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs. Association for Computing Machinery , New York, NY, USA, 118\u2013131. https:\/\/doi.org\/10.1145\/3293880.3294097 10.1145\/3293880.3294097 Y. Forster, S. Sch\u00e4fer, S. Spies, and K. Stark. 2019. Call-by-Push-Value in Coq: Operational, Equational, and Denotational Theory. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs. Association for Computing Machinery, New York, NY, USA, 118\u2013131. https:\/\/doi.org\/10.1145\/3293880.3294097"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201353"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_3_2_1_10_1","unstructured":"H. Herbelin. 1995. S\u00e9quents qu\u2019on calcule\u00a0: de l\u2019interpr\u00e9tation du calcul des s\u00e9quents comme calcul de \u03bb -termes et comme calcul de strat\u00e9gies gagnantes. Th\u00e8se d\u2019universit\u00e9. Universit\u00e9 Paris 7.  H. Herbelin. 1995. S\u00e9quents qu\u2019on calcule\u00a0: de l\u2019interpr\u00e9tation du calcul des s\u00e9quents comme calcul de \u03bb -termes et comme calcul de strat\u00e9gies gagnantes. Th\u00e8se d\u2019universit\u00e9. Universit\u00e9 Paris 7."},{"key":"e_1_3_2_1_11_1","volume-title":"7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005, Proceedings(Lecture Notes in Computer Science), P.\u00a0Urzyczyn (Ed.). Vol.\u00a03461","author":"Herbelin H.","year":"2005","unstructured":"H. Herbelin . 2005 . On the Degeneracy of Sigma-Types in Presence of Computational Classical Logic. In Typed Lambda Calculi and Applications , 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005, Proceedings(Lecture Notes in Computer Science), P.\u00a0Urzyczyn (Ed.). Vol.\u00a03461 . Springer, 209\u2013220. https:\/\/doi.org\/10.1007\/11417170_16 10.1007\/11417170_16 H. Herbelin. 2005. On the Degeneracy of Sigma-Types in Presence of Computational Classical Logic. In Typed Lambda Calculi and Applications, 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005, Proceedings(Lecture Notes in Computer Science), P.\u00a0Urzyczyn (Ed.). Vol.\u00a03461. Springer, 209\u2013220. https:\/\/doi.org\/10.1007\/11417170_16"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9018-9"},{"volume-title":"Call-by-Push-Value: A Subsuming Paradigm","author":"Levy P.B.","key":"e_1_3_2_1_13_1","unstructured":"P.B. Levy . 1999. Call-by-Push-Value: A Subsuming Paradigm . In Typed Lambda Calculi and Applications, Jean-Yves Girard (Ed.). Springer , Berlin, Heidelberg , 228\u2013243. P.B. Levy. 1999. Call-by-Push-Value: A Subsuming Paradigm. In Typed Lambda Calculi and Applications, Jean-Yves Girard (Ed.). Springer, Berlin, Heidelberg, 228\u2013243."},{"volume-title":"V. 2)","author":"Levy P.B.","key":"e_1_3_2_1_14_1","unstructured":"P.B. Levy . 2001. Call-By-Push-Value : A Functional\/Imperative Synthesis (Semantics Structures in Computation , V. 2) . Kluwer Academic Publishers , USA. P.B. Levy. 2001. Call-By-Push-Value: A Functional\/Imperative Synthesis (Semantics Structures in Computation, V. 2). Kluwer Academic Publishers, USA."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-0480-6"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_3_2_1_17_1","volume-title":"TYPES Workshop, at B\u01cestad","author":"Parigot M.","year":"1993","unstructured":"M. Parigot . 1993 . Classical Proofs as Programs. In Kurt G\u00f6del Colloquium. 263\u2013276 . Presented at TYPES Workshop, at B\u01cestad , June 1992. M. Parigot. 1993. Classical Proofs as Programs. In Kurt G\u00f6del Colloquium. 263\u2013276. Presented at TYPES Workshop, at B\u01cestad, June 1992."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"}],"event":{"name":"PPDP 2023: International Symposium on Principles and Practice of Declarative Programming","acronym":"PPDP 2023","location":"Lisboa Portugal"},"container-title":["International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3610612.3610613","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:36:00Z","timestamp":1750178160000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3610612.3610613"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,22]]},"references-count":18,"alternative-id":["10.1145\/3610612.3610613","10.1145\/3610612"],"URL":"https:\/\/doi.org\/10.1145\/3610612.3610613","relation":{},"subject":[],"published":{"date-parts":[[2023,10,22]]},"assertion":[{"value":"2023-10-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}