We propose a core calculus for programming languages with effects, interpreted using a hypergraph-rewriting abstract machine. The intrinsic calculus syntax and semantics only deals with the basic structural aspects of programming languages: variables, names, and thunks. 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 observational equivalence in languages with effects. We illustrate and motivate the basic ideas with some challenging examples from the literature.
Joint work with Koko Muroya (RIMS, Kyoto)