Skip to Main content Skip to Navigation
Conference papers

A Flexible Categorial Formalisation of Term Graphs as Directed Hypergraphs

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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [11 references]  Display  Hide  Download

https://hal.inria.fr/hal-02364572
Contributor : Hal Ifip <>
Submitted on : Friday, November 15, 2019 - 9:03:09 AM
Last modification on : Friday, November 15, 2019 - 9:05:05 AM
Long-term archiving on: : Sunday, February 16, 2020 - 1:14:42 PM

File

 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2022-01-01

Please log in to resquest access to the document

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

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⟩

Share

Metrics

Record views

86