ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Tue 9 Apr 2019 14:00 - 14:30 at SUN II - Program Semantics Chair(s): Andrzej Murawski

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 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:00 - 16:00
Program SemanticsESOP at SUN II
Chair(s): Andrzej Murawski University of Oxford
14:00
30m
Talk
Extended call-by-push-value: reasoning about effectful programs and evaluation orderBest paper nomination
ESOP
Dylan McDermott University of Cambridge, Alan Mycroft University of Cambridge
Link to publication
14:30
30m
Talk
Effectful Normal-Form Bisimulation
ESOP
Ugo Dal Lago University of Bologna / Inria, Francesco Gavazzo
Link to publication
15:00
30m
Talk
On the Multi-Language Construction
ESOP
Samuele Buro Università degli Studi di Verona, Isabella Mastroeni University of Verona, Italy
Link to publication
15:30
30m
Talk
Probabilistic Programming Inference via Intensional Semantics
ESOP
Simon Castellan Imperial College London, UK, Hugo Paquet University of Cambridge
Link to publication