A Flexible Categorial Formalisation of Term Graphs as Directed Hypergraphs

Abstract

Term graphs are the concept at the core of important implementation techniques for functional programming languages, and are also used as internal data structures in many other symbolic computation setting, including in code generation back-ends for example in compilers. To our knowledge, there are no formally verified term graph manipulation systems so far; we present an approach to formalising term graphs, as a relatively complex example of …