文章基本信息

标题：Dependently-Typed Formalisation of Typed Term Graphs
本地全文：下载
作者：Wolfram Kahl
期刊名称：Electronic Proceedings in Theoretical Computer Science
电子版ISSN：2075-2180
出版年度：2011
卷号：48
页码：38-53
DOI：10.4204/EPTCS.48.6
出版社：Open Publishing Association
摘要：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.