Dependently-Typed Formalisation of Typed Term Graphs

被引:2
作者
Kahl, Wolfram [1 ]
机构
[1] McMaster Univ, Hamilton, ON L8S 4L8, Canada
关键词
D O I
10.4204/EPTCS.48.6
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
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.
引用
收藏
页码:38 / 53
页数:16
相关论文
共 19 条
[1]  
Anand CK, 2009, CH CRC COMP SCI SER, P3
[2]   An Optimized Cell BE Special Function Library Generated by Coconut [J].
Anand, Christopher Kumar ;
Kahl, Wolfram .
IEEE TRANSACTIONS ON COMPUTERS, 2009, 58 (08) :1126-1138
[3]  
Anand CK, 2008, LECT NOTES COMPUT SC, V5088, P217
[4]  
ARIOLA ZM, 1994, IEEE S LOG, P416, DOI 10.1109/LICS.1994.316066
[5]   HYPEREDGE REPLACEMENT JUNGLE REWRITING FOR TERM-REWRITING SYSTEMS AND LOGIC PROGRAMMING [J].
CORRADINI, A ;
ROSSI, F .
THEORETICAL COMPUTER SCIENCE, 1993, 109 (1-2) :7-48
[6]   An algebraic presentation of term graphs, via GS-monoidal categories [J].
Corradini, A ;
Gadducci, F .
APPLIED CATEGORICAL STRUCTURES, 1999, 7 (04) :299-331
[7]  
Gonzalia C., 2006, THESIS
[8]  
HAEBERER AM, 1997, RELATIONAL METHODS C, P54
[9]  
HOFFMANN B, 1991, RAIRO-INF THEOR APPL, V25, P445, DOI 10.1051/ita/1991250504451
[10]  
Huet G, 2000, FOUNDAT COMPUT, P239