The next 700 abstract machines

We propose a new core calculus for programming languages with effects,
interpreted using a hypergraph-rewriting abstract machine inspired by
the Geometry of Interaction. 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.

Joint work with Koko Muroya and Todd Waugh Ambridge.