EAPLS Best Paper Award 2019

The EAPLS Best Paper Award 2019 is awarded to the paper

 "Extended call-by-push-value: reasoning about effectful programs and evaluation order", by Dylan McDermott and Alan Mycroft (University of Cambridge).

 This paper has been published in the proceedings of the 28th European Symposium on Programming (ESOP 2019). Congratulations to the authors!

The abstract of the paper:

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.

Link to publication:

https://link.springer.com/chapter/10.1007/978-3-030-17184-1_9