Dependently-Typed Formalisation of Typed Term Graphs

Wolfram Kahl
(McMaster University)

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.

In Rachid Echahed: Proceedings 6th International Workshop on Computing with Terms and Graphs (TERMGRAPH 2011), Saarbrücken, Germany, 2nd April 2011, Electronic Proceedings in Theoretical Computer Science 48, pp. 38–53.
Published: 11th February 2011.
ArXived at: https://dx.doi.org/10.4204/EPTCS.48.6 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org