Dependently-Typed Formalisation of Typed Term Graphs
Logic in Computer Science
2011-02-15 v1 Programming Languages
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.
Keywords
Cite
@article{arxiv.1102.2653,
title = {Dependently-Typed Formalisation of Typed Term Graphs},
author = {Wolfram Kahl},
journal= {arXiv preprint arXiv:1102.2653},
year = {2011}
}
Comments
In Proceedings TERMGRAPH 2011, arXiv:1102.2268