Dependently-Typed Formalisation of Typed Term Graphs
Wolfram Kahl (McMaster University)
TL;DR
This paper explores formalising typed and untyped term graphs using dependently-typed programming in Agda, leveraging category theory and variable-binding abstractions to enhance correctness and expressiveness.
Contribution
It introduces a formalisation of term graphs in Agda employing gs-monoidal categories and variable-binding libraries, combining category theory with dependently-typed programming.
Findings
Successful formalisation of term graphs in Agda
Integration of category theory with dependently-typed programming
Enhanced correctness guarantees for term graph representations
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.