arXiv subjects
Publications and source records attributed to Wolfram Kahl.
Term graph rewriting is important as "conceptual implementation" of the execution of functional programs, and of data-flow optimisations in compilers. One way to define term graph transformation rule application is via the well-established and intuitively accessible double-pushout (DPO) approach; we present a new result proving semantics preservation for such DPO-based term graph rewriting.
Due to their "inherent parallelism", interaction nets have since their introduction been considered as an attractive implementation mechanism for functional programming. We show that a simple highly-concurrent implementation in Haskell can achieve promising speed-ups on multiple cores.
We employ the dependently-typed programming language Agda2 to explore formalisation of untyped and typed term graphs directly as set-based graph structures, via the gs-monoidal categories of Corradini and Gadducci, and as nested let-expressions using Pouillard and Pottier's NotSoFresh library of variable-binding abstractions.