Yannick Forster, Steven Schäfer, Simon Spies, Kathrin Stark: Call-by-push-value in coq: operational, equational, and denotational theory. CPP 2019: 118-131