It looks like a lambda calculus with effectful computations that can model imperative programming. I hadn't heard of it before either.

https://en.wikipedia.org/wiki/Call-by-push-value

This article was previously on HN and is a good explainer: https://thunderseethe.dev/posts/bet-on-cbpv/

HN discussion: https://news.ycombinator.com/item?id=39653895

The basic point is to have something akin to lambda-calculus that can equally account for both strict and lazy evaluation strategies, in a way that doesn't unduly sacrifice expressiveness for one or the other. (Compare the ML family of languages and Haskell, where strict and lazy evaluation respectively are idiomatic. You can express lazy evaluation in a ML and strict evaluation in Haskell, but only in clunky ways that don't align with the overall logic of the language. CBPV and other comparable formalisms aim to resolve this.)