Extended call-by-push-value: reasoning about effectful programs and evaluation orderBest paper nomination
Traditionally, reasoning about programs under varying evaluation regimes (call-by-value, call-by-name etc.) was done at the meta-level, treating them as term rewriting systems. Levy’s call-by-push-value (CBPV) calculus provides a more powerful approach for reasoning, by treating CBPV terms as a common intermediate language which captures both call-by-value and call-by-name, and by allowing equational reasoning about changes to evaluation order between or within programs.
We extend CBPV to additionally deal with call-by-need, which is non-trivial because of shared reductions. This allows the equational reasoning to also support call-by-need. As an example, we then prove that call-by-need and call-by-name are equivalent if nontermination is the only side-effect in the language.
We then show how to incorporate an effect system. This enables us to exploit static knowledge of the potential effects of a given expression to augment equational reasoning; thus a program fragment might be invariant under change of evaluation regime only because of knowledge of its effects.
Tue 9 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 16:00 | |||
14:00 30mTalk | Extended call-by-push-value: reasoning about effectful programs and evaluation orderBest paper nomination ESOP Link to publication | ||
14:30 30mTalk | Effectful Normal-Form Bisimulation ESOP Link to publication | ||
15:00 30mTalk | On the Multi-Language Construction ESOP Link to publication | ||
15:30 30mTalk | Probabilistic Programming Inference via Intensional Semantics ESOP Link to publication |