A Flexible Categorial Formalisation of Term Graphs as Directed Hypergraphs - Archive ouverte HAL Access content directly
Conference Papers Year : 2019

A Flexible Categorial Formalisation of Term Graphs as Directed Hypergraphs

(1) , (1)
1
Wolfram Kahl
  • Function : Author
  • PersonId : 1058308
Yuhang Zhao
  • Function : Author
  • PersonId : 1058309

Abstract

Term graphs are the concept at the core of important implementation techniques for functional programming languages, and are also used as internal data structures in many other symbolic computation setting, including in code generation back-ends for example in compilers. To our knowledge, there are no formally verified term graph manipulation systems so far; we present an approach to formalising term graphs, as a relatively complex example of graph structures, in the dependently-typed programming language and proof system Agda in a way that both the mathematical theory and useful executable implementations can be obtained as instances of the same abstract definition.
Fichier principal
Vignette du fichier
486157_1_En_6_Chapter.pdf (537.62 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-02364572 , version 1 (15-11-2019)

Licence

Attribution - CC BY 4.0

Identifiers

Cite

Wolfram Kahl, Yuhang Zhao. A Flexible Categorial Formalisation of Term Graphs as Directed Hypergraphs. 24th International Workshop on Algebraic Development Techniques (WADT), Jul 2018, Egham, United Kingdom. pp.103-118, ⟨10.1007/978-3-030-23220-7_6⟩. ⟨hal-02364572⟩
44 View
9 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More