Open call-by-push-value

Abstract

Call-By-Push-Value (CBPV) is a model of computation that allows to reconcile the Call-By-Name (CBN) and Call-By-Value (CBV) evaluation strategies on closed terms. Unfortunately, its extension to open terms faces the same problems as CBV: some redexes get stuck. Several solutions have been presented for CBV but not for CBPV. We show that a representative fragment of $LJ^η_p$ (a polarised intuitionnistic abstract-machine-like calculi) is equivalent to CBPV on closed terms, and equip it with a notion of weak reduction on open terms.

Publication
M2 report

Most of part 1 and 2 are subsumed by Untyped polarized calculi. Part 3 is subsumed by Solvability in a polarized calculus.

PhD student

Related