Isn't CBPV more of a way of accounting for both strict (call-by-value) and lazy (call-by-name) evaluation in the same programming language? Not sure how that would help wrt. static memory management.
Call by Push Value does account for both CbV and CbN language semantics, but the reason it can do so is by basing the language in a rather particular categorical semantic.
Based on the linked intro, it would seem that the language is leveraging the ‘computational’ types that are an intrinsic part of the CBPV semantics to force the ‘thunking’ of the dependent types. Effectively, all of the types become ‘functions’ from the CBPV lense and those functions are linear by construction (it is a categorical, as in category theory, feature of the underlying semantics). Although not cited, it seems like the underlying type theory takes notice and inspiration from Levy’s work on adjunction models for CBPV.
I tried to find a way to make this comment that wasn’t too acedemic sounding, but I think I missed the mark.
