带依赖类型的类型化项图形式化
计算机科学中的逻辑
2011-02-15 v1 编程语言
摘要
我们采用依赖类型编程语言Agda2，探索将无类型和类型化项图直接形式化为基于集合的图结构（通过Corradini和Gadducci的gs-幺半范畴），以及使用Pouillard和Pottier的NotSoFresh变量绑定抽象库将其形式化为嵌套let表达式。
引用
@article{arxiv.1102.2653,
title = {Dependently-Typed Formalisation of Typed Term Graphs},
author = {Wolfram Kahl},
journal= {arXiv preprint arXiv:1102.2653},
year = {2011}
}
备注
In Proceedings TERMGRAPH 2011, arXiv:1102.2268