TERMGRAPH 2020 Keynote: Hypernet Semantics of Programming Languages
by Dan R. Ghica
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)
Talk given at Termgraph 2020.