Dependently-Typed Formalisation of Typed Term Graphs
Abstract
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.