ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Sat 6 Apr 2019 10:00 - 10:30 at S1 (PERR) - I

We propose a new core calculus for programming languages with effects which is interpreted using a hypergraph-rewriting abstract machine inspired by the Geometry of Inter- action. The intrinsic calculus syntax and semantics only deals with the basic structural aspects of programming languages: variable binding, name binding, and thunking. Everything else, including function abstraction and application, must be provided as extrinsic operations with associated rewrite rules. The graph representation yields natural concepts of locality and robustness for equational properties and reduction rules, which enable a novel flexible and powerful reasoning methodology about (type-free) languages with effects. We illustrate and motivate the technique with challenging examples from the literature.

Sat 6 Apr

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

09:00 - 10:30
Invited talk by Margus Veanes
Margus Veanes Microsoft Research
Local Reasoning for Robust Observational Equivalence
Dan Ghica University of Birmingham, Koko Muroya RIMS, Kyoto University, JP & University of Birmingham, UK, Todd Waugh Ambridge University of Birmingham