[rntz]

> I think that Call-by-push-value can help us with both recovering the benefits of laziness as well as reasoning about effects.

I would be very interested to hear why you think that, or just have some links on the subject. In particular it's not clear to me how CBPV helps us reason about effects.

[jonsterling]

It might help to read Levy's thesis, which is source on CBPV. Also read the literature on Conor McBride's Frank, which is based on a variant of CBPV.