{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:30:53Z","timestamp":1767929453338,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":23,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,1,14]],"date-time":"2019-01-14T00:00:00Z","timestamp":1547424000000},"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":[[2019,1,14]]},"DOI":"10.1145\/3293880.3294097","type":"proceedings-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:56Z","timestamp":1546608836000},"page":"118-131","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Call-by-push-value in Coq: operational, equational, and denotational theory"],"prefix":"10.1145","author":[{"given":"Yannick","family":"Forster","sequence":"first","affiliation":[{"name":"Saarland University, Germany"}]},{"given":"Steven","family":"Sch\u00e4fer","sequence":"additional","affiliation":[{"name":"Saarland University, Germany"}]},{"given":"Simon","family":"Spies","sequence":"additional","affiliation":[{"name":"Saarland University, Germany"}]},{"given":"Kathrin","family":"Stark","sequence":"additional","affiliation":[{"name":"Saarland University, Germany"}]}],"member":"320","published-online":{"date-parts":[[2019,1,14]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Coq proof assistant. 2018. http:\/\/coq.inria.fr.  Coq proof assistant. 2018. http:\/\/coq.inria.fr."},{"key":"e_1_3_2_1_2_1","unstructured":"Karl Crary. 2009. A simple proof of call-by-value standardization. Computer Science Department (2009) 474 (2009).  Karl Crary. 2009. A simple proof of call-by-value standardization. Computer Science Department (2009) 474 (2009)."},{"key":"e_1_3_2_1_3_1","unstructured":"Christian Doczkal and Jan Schwinghammer. 2007. A Proof of Strong Normalization for Call-by-push-value. Unpublished note. http:\/\/www.ps.uni-saarland.de\/Publications\/details\/Doczkal.Schwinghammer.07.html  Christian Doczkal and Jan Schwinghammer. 2007. A Proof of Strong Normalization for Call-by-push-value. Unpublished note. http:\/\/www.ps.uni-saarland.de\/Publications\/details\/Doczkal.Schwinghammer.07.html"},{"key":"e_1_3_2_1_4_1","unstructured":"Derek Dreyer Ralf Jung Jan-Oliver Kaiser Hoang-Hai Dang and David Swasey. 2018. Semantics of Type Systems - Lecture Notes. (2018).  Derek Dreyer Ralf Jung Jan-Oliver Kaiser Hoang-Hai Dang and David Swasey. 2018. Semantics of Type Systems - Lecture Notes. (2018)."},{"key":"e_1_3_2_1_5_1","unstructured":"Yannick Forster. 2016. On the expressive power of effect handlers and monadic reflection. MPhil thesis University of Cambridge. (2016). https:\/\/www.ps.uni-saarland.de\/~forster\/downloads\/mphil-thesis.pdf  Yannick Forster. 2016. On the expressive power of effect handlers and monadic reflection. MPhil thesis University of Cambridge. (2016). https:\/\/www.ps.uni-saarland.de\/~forster\/downloads\/mphil-thesis.pdf"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110257"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Yannick Forster Steven Sch\u00e4fer Simon Spies and Kathrin Stark. 2018. Appendix for Call-By-Push-Value in Coq: Operational Equational and Denotational Theory. https:\/\/ps.uni-saarland.de\/cbpv-in-coq.  Yannick Forster Steven Sch\u00e4fer Simon Spies and Kathrin Stark. 2018. Appendix for Call-By-Push-Value in Coq: Operational Equational and Denotational Theory. https:\/\/ps.uni-saarland.de\/cbpv-in-coq.","DOI":"10.1145\/3293880.3294097"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"e_1_3_2_1_9_1","volume-title":"Abella and Beluga. In LIPIcs-Leibniz International Proceedings in Informatics","volume":"84","author":"Kaiser Jonas","year":"2017"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167098"},{"key":"e_1_3_2_1_11_1","volume-title":"International Symposium on Code Generation and Optimization.","author":"Lei\u00dfa Roland","year":"2015"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/645894.671755"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-0480-6"},{"key":"e_1_3_2_1_14_1","volume-title":"Call-by-push-value: A Functional\/imperative Synthesis.","author":"Levy Paul Blain","year":"2012"},{"key":"e_1_3_2_1_15_1","unstructured":"John C Mitchell. 1996. Foundations for programming languages. Vol. 1. MIT press Cambridge.   John C Mitchell. 1996. Foundations for programming languages . Vol. 1. MIT press Cambridge."},{"key":"e_1_3_2_1_16_1","first-page":"1","volume-title":"ACM SIGPLAN Notices","volume":"31","author":"Jones Simon Peyton","year":"1996"},{"key":"e_1_3_2_1_17_1","unstructured":"Andrew Pitts. 2005. Typed operational reasoning. Advanced Topics in Types and Programming Languages (2005) 245-289.  Andrew Pitts. 2005. Typed operational reasoning. Advanced Topics in Types and Programming Languages (2005) 245-289."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94821-8_31"},{"key":"e_1_3_2_1_19_1","volume-title":"Embedding Higher-Order Abstract Syntax in Type Theory. In Abstract for Types Workshop.","author":"Sch\u00e4fer Steven","year":"2018"},{"key":"e_1_3_2_1_20_1","first-page":"41","article-title":"A new look at generalized rewriting in type theory","volume":"2","author":"Sozeau Matthieu","year":"2010","journal-title":"Journal of formalized reasoning"},{"key":"e_1_3_2_1_21_1","volume-title":"Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs.","author":"Stark Kathrin","year":"2018"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"William W Tait. 1967. Intensional interpretations of functionals of finite type I. The journal of symbolic logic 32 2 (1967) 198-212.  William W Tait. 1967. Intensional interpretations of functionals of finite type I. The journal of symbolic logic 32 2 (1967) 198-212.","DOI":"10.2307\/2271658"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80045-8"}],"event":{"name":"CPP '19: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Cascais Portugal","acronym":"CPP '19","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3293880.3294097","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3293880.3294097","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:50Z","timestamp":1750207430000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3293880.3294097"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,14]]},"references-count":23,"alternative-id":["10.1145\/3293880.3294097","10.1145\/3293880"],"URL":"https:\/\/doi.org\/10.1145\/3293880.3294097","relation":{},"subject":[],"published":{"date-parts":[[2019,1,14]]},"assertion":[{"value":"2019-01-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}