Operational Semantics with Hierarchical Abstract Syntax Graphs
Dan R. Ghica (Huawei Research, Edinburgh, University of Birmingham,, UK)

TL;DR
This paper introduces a graphical approach to semantic analysis of programming languages using hierarchical abstract syntax graphs, enabling uniform representation of various language features and facilitating reasoning about program equivalence.
Contribution
It presents a novel graphical semantics framework that unifies structural operational semantics and abstract machines, improving reasoning about contextual equivalence.
Findings
Graphs automatically handle alpha-equivalence
Framework describes pure computation, store, and control uniformly
Offers new methods for reasoning about contextual equivalence
Abstract
This is a motivating tutorial introduction to a semantic analysis of programming languages using a graphical language as the representation of terms, and graph rewriting as a representation of reduction rules. We show how the graphical language automatically incorporates desirable features, such as alpha-equivalence and how it can describe pure computation, imperative store, and control features in a uniform framework. The graph semantics combines some of the best features of structural operational semantics and abstract machines, while offering powerful new methods for reasoning about contextual equivalence. All technical details are available in an extended technical report by Muroya and the author and in Muroya's doctoral dissertation.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Semantic Web and Ontologies · Model-Driven Software Engineering Techniques
