%0 Conference Proceedings
%T A Flexible Categorial Formalisation of Term Graphs as Directed Hypergraphs
%+ McMaster University [Hamilton, Ontario]
%A Kahl, Wolfram
%A Zhao, Yuhang
%Z Part 3: Contributed Papers
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 24th International Workshop on Algebraic Development Techniques (WADT)
%C Egham, United Kingdom
%Y José Luiz Fiadeiro
%Y Ionuț Țuțu
%I Springer International Publishing
%3 Recent Trends in Algebraic Development Techniques
%V LNCS-11563
%P 103-118
%8 2018-07-02
%D 2018
%R 10.1007/978-3-030-23220-7_6
%Z Computer Science [cs]Conference papers
%X 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.
%G English
%Z TC 1
%Z WG 1.3
%2 https://inria.hal.science/hal-02364572/document
%2 https://inria.hal.science/hal-02364572/file/486157_1_En_6_Chapter.pdf
%L hal-02364572
%U https://inria.hal.science/hal-02364572
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-TC1
%~ IFIP-WG1-3
%~ IFIP-WADT
%~ IFIP-LNCS-11563