Call-by-push-value, often abbreviated as CBPV, is a system which uses modalities to control the evaluation order/calling mechanism used. It was first discovered and studied by Paul Blain Levy.
The design of CBPV is empirical: its primitives seem to arise as common structure observed in many settings and previous systems. They are not necessarily canonical or inescapable.[1]
There is an extensive book length treatment of CBPV:
Levy, Paul Blain. 2003. Call-by-Push-Value: A Functional-Imperative Synthesis. Semantic Structures in Computation. Springer. https://doi.org/10.1007/978-94-007-0954-6.
@book{levy_2003,
series = {Semantic {Structures} in {Computation}},
title = {Call-by-{Push}-{Value}: {A} {Functional}-{Imperative} {Synthesis}},
isbn = {978-94-010-3752-5},
publisher = {Springer},
author = {Levy, Paul Blain},
year = {2003},
doi = {10.1007/978-94-007-0954-6}
}
Before that, there was a journal paper:
Levy, Paul Blain. 2006. ‘Call-by-Push-Value: Decomposing Call-by-Value and Call-by-Name’. Higher-Order and Symbolic Computation 19 (4): 377–414. https://doi.org/10.1007/s10990-006-0480-6. pdf
@article{levy_2006,
title = {Call-by-push-value: {Decomposing} call-by-value and call-by-name},
volume = {19},
issn = {1388-3690},
url = {https://www.cs.bham.ac.uk/~pbl/papers/hosc05.pdf},
doi = {10.1007/s10990-006-0480-6},
number = {4},
journal = {Higher-Order and Symbolic Computation},
author = {Levy, Paul Blain},
month = dec,
year = {2006},
keywords = {Call-by-name, Call-by-push-value, Call-by-value, Computational effect, Lambda-calculus, Monad},
pages = {377--414}
CBPV first appeared at TLCA 1999:
Levy, Paul Blain. 1999. ‘Call-by-Push-Value: A Subsuming Paradigm’. In Typed Lambda Calculi and Applications, edited by Jean-Yves Girard, 1581:228–43. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-48959-2_17.
@inproceedings{levy_1999,
address = {Berlin, Heidelberg},
series = {Lecture {Notes} in {Computer} {Science}},
title = {Call-by-{Push}-{Value}: {A} {Subsuming} {Paradigm}},
volume = {1581},
doi = {10.1007/3-540-48959-2_17},
language = {en},
urldate = {2020-09-13},
booktitle = {Typed {Lambda} {Calculi} and {Applications}},
publisher = {Springer Berlin Heidelberg},
author = {Levy, Paul Blain},
editor = {Goos, Gerhard and Hartmanis, Juris and van Leeuwen, Jan and Girard, Jean-Yves},
year = {1999},
pages = {228--243}
}
This point was reinforced by Paul Levy in an invited talk at HOPE 2020 @ ICFP 2020. ↩︎