Local Reasoning for Robust Observational Equivalence
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
|09:00 - 10:00|
Margus VeanesMicrosoft Research
|10:00 - 10:30|