Yannick Forster, Steven Schäfer, Simon Spies, Kathrin Stark. Call-by-push-value in coq: operational, equational, and denotational theory. In Assia Mahboubi, Magnus O. Myreen, editors, Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019. pages 118-131, ACM, 2019. [doi]
Abstract is missing.