# Operational Semantics with Hierarchical Abstract Syntax Graphs

@inproceedings{Ghica2020OperationalSW, title={Operational Semantics with Hierarchical Abstract Syntax Graphs}, author={Dan R. Ghica}, booktitle={TERMGRAPH@FSCD}, year={2020} }

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 α-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… Expand

#### One Citation

Functorial String Diagrams for Reverse-Mode Automatic Differentiation

- Computer Science
- ArXiv
- 2021

To give an efficient yet principled implementation of the AD algorithm, a sound and complete representation of hierarchical string diagrams is defined as a class of hierarchical hypergraphs the authors call hypernets. Expand

#### References

SHOWING 1-10 OF 35 REFERENCES

Local Reasoning for Robust Observational Equivalence

- Computer Science
- ArXiv
- 2019

A new core calculus for programming languages with effects is proposed, interpreted using a hypergraph-rewriting abstract machine inspired by the Geometry of Interaction, which yields natural concepts of locality and robustness for equational properties and reduction rules. Expand

Operational Semantics and Program Equivalence

- Computer Science
- APPSEM
- 2000

This tutorial paper discusses a particular style of operational semantics that enables one to give a 'syntax-directed' inductive definition of termination which is very useful for reasoning about… Expand

A Categorical and Graphical Treatment of Closure Conversion

- Computer Science
- MFPS
- 1999

Using closure conversion, this paper can prove normalization results for both normal forms of graphs, and obtain sound algorithms for compiling the language into either procedural or object-oriented code. Expand

Hypernet semantics of programming languages

- Computer Science
- 2020

This thesis proposes a semantical framework based on abstract machines that enables analysis of program execution cost and direct proof of program equivalence, and enjoys novel flexibility. Expand

Reasoning about local variables with operationally-based logical relations

- Mathematics, Computer Science
- Proceedings 11th Annual IEEE Symposium on Logic in Computer Science
- 1996

A parametric logical relation between the phrases of an Algol-like language is presented and provides an applicative characterisation of contextual equivalence for the language and provides a useful (and complete) method for proving equivalences. Expand

Nominal Sets: Names and Symmetry in Computer Science

- Computer Science
- 2013

The author provides an introduction to the basic theory of nominal sets and surveys some of the applications that have developed in programming language semantics, functional programming and logic programming. Expand

Full Abstraction for Signal Flow Graphs

- Computer Science
- POPL 2015
- 2015

This paper equips signal flow graphs with a structural operational semantics, and classifies the ways in which any graph can be realised -- rewritten, using the graphical theory, into an executable form where the operational behavior and the denotation coincides. Expand

Proof Nets and the Linear Substitution Calculus

- Mathematics, Computer Science
- ICTAC
- 2018

It is shown that the linear substitution calculus, a simple refinement of the \(\lambda \)-calculus with sharing, is isomorphic to proof nets at the operational level. Expand

A Syntactic Approach to Type Soundness

- Computer Science, Mathematics
- Inf. Comput.
- 1994

A new approach to proving type soundness for Hindley/Milner-style polymorphic type systems by an adaptation of subject reduction theorems from combinatory logic to programming languages and the use of rewriting techniques for the specification of the language semantics is presented. Expand

Memoryful geometry of interaction: from coalgebraic components to algebraic effects

- Computer Science
- CSL-LICS
- 2014

Abramsky's idea of resumption based GoI is developed systematically into a generic framework that accounts for computational effects (nondeterminism, probability, exception, global states, interactive I/O, etc.) and the resulting interpretation is shown to be sound. Expand