TERMGRAPH 2026
14th International Workshop on Computing with Terms and Graphs
Lisbon, Portugal
19 July 2026 (one-day workshop)
Background and history
Graphs, and graph transformation systems, are used in many areas
within Computer Science: to represent data structures and algorithms,
to define computation models, as a general modelling tool to study
complex systems, etc.
Research in term and graph rewriting ranges from theoretical
questions to practical implementation issues. Different research areas
include: the modelling of first- and higher-order term rewriting by
(acyclic or cyclic) graph rewriting, the use of graphical frameworks
such as interaction nets and sharing graphs (optimal reduction), rewrite
calculi for the semantics and analysis of functional programs, graph
reduction implementations of programming languages, graphical calculi
modelling concurrent and mobile computations, object-oriented systems,
graphs as a model of biological or chemical systems, quantum
computing, and automated reasoning and symbolic computation systems
working on shared structures.
Previous editions of TERMGRAPH took place in Barcelona (2002), Rome
(2004), Vienna (2006), Braga (2007), York (2009), Saarbrücken (2011),
Rome (2013), Vienna (2014), Eindhoven (2016), Oxford (2018), online
(2020, planned to be held in Paris), Haifa (2022), and Luxembourg (2024).
The
permanent TERMGRAPH
website has further information.
Aim
The aim of this workshop is to bring together researchers working in
these different domains, to foster their interaction, to provide a
forum for presenting new ideas and work in progress, and to enable
newcomers to learn about current activities in this area.
Topics of Interest
Topics of interest include all aspects of term-/graph rewriting
(term-graph and graph rewriting) and applications of graph
transformations in programming, automated reasoning and symbolic
computation. This includes (but is not limited to):
- theory of first-order and higher-order term and graph rewriting
- graph rewriting in lambda calculus (sharing graphs, optimality)
- term-/graph based models of computation
- graph grammars
- term-/graph based languages and modelling frameworks
- term-/graph rewriting tools:
- system descriptions, and case studies
- applications of term-/graph rewriting in,
and term-/graph rewriting aspects of:
- semantics and implementation of programming languages
- compiler construction
- interaction nets and proof nets
- string diagrams
- software engineering
- automated reasoning and symbolic computation
- functional and logic programming
- pattern recognition
- Machine Learning (Graph Neural Networks)
- bioinformatics
- quantum computing
Call for Papers
We invite submissions of
extended abstracts of
at most 8 pages
in
EPTCS style
(see also
template on
Overleaf). This may include, concerning any of the topics above:
- original work,
- tutorials,
- work in progress,
- system descriptions of term-/graph rewriting tools.
Extended abstracts have to be submitted
no later than
27 April 2026 (AoE)
electronically (pdf) via:
Papers will be judged on relevance, originality, correctness, and
usefulness.
After the workshop, authors of presented extended abstracts will be
invited to submit a longer version of their work
(a 15-page paper) for the publication
of the Workshop Post-Proceedings
in EPTCS (Electronic Proceedings in
Theoretical Computer Science) These submissions will undergo a
second round of refereeing with:
- submission deadline in the mid of October 2026,
- notification in December 2026,
- publication in February 2027.
Important Dates (AoE)
- Extended submission deadlines:
- Titles and short abstracts: Wednesday, 6 May 2026
- Extended abstracts: Monday, 11 May 2026
- Notification: Wednesday, 27 May 2026
- Program publication: Wednesday, 3 June 2026
- Final pre-proceedings version (8 pages excluding references) due: Monday, 15 June 2026
- Workshop: 19 July 2026
Invited Speakers
-
Dan R. Ghica, Huawei Central Software Institute & University of Birmingham, UK
(Joint keynote with
DIALOCO 2026)
Syntactic trinitarianism: terms, graphs, diagrams
The concept of 'syntax' is commonly understood as the structure hidden
in linear sequences of tokens, which in language and logic we commonly
call ‘terms’. However, for the purpose of analysis and transformation,
compilers use more efficient data structures to represent syntax,
namely graphs. The gap between the linear (term) and graph syntax is
elegantly bridged by a third formalism, namely that of string
diagrams, a planar representation of terms in the categorical
representation of syntax. In this talk I will show how the interplay
of terms, graphs, and diagrams can help specify and implement complex
analyses and transformations in compilers for higher-order programming
languages, such as type inference, automatic differentiation, or
closure conversion. This methodology is at the foundation of a new
industrial-strength compiler being implemented currently at Huawei.
Most of the material I will discuss is based on the recent tutorial
paper “Hierarchical string diagrams and applications” jointly with
Fabio Zanasi (https://arxiv.org/abs/2305.18945) about to appear as a
CUP monograph.
-
Nicolas Troquard, Gran Sasso Science Institute, Italy
Graph Neural Networks, Their Logics, and Formal Verification
Graph Neural Networks are deep learning models designed to process
graph-structured data. Most modern GNNs operate by message passing:
node representations are updated through repeated rounds of
aggregating and combining information from neighboring nodes. This
makes them well suited to applications involving relational and
networked structures, and also places them naturally in dialogue with
topics from graph rewriting and graph-based computation.
In this talk, we present recent results on the relationship between
Graph Neural Networks and formal logic, with the choice of topics
guided by the speaker's own research in the area. We introduce logics
that precisely capture the expressive power of certain classes of
integer-valued GNNs, and show how GNN computations can be translated
into logical formulas. We also discuss variants of GNNs over finite
computer number formats. These logical characterizations provide a
foundation for formal verification, allowing us to establish
complexity bounds for key reasoning problems about GNN behavior.
-
Vincent van Oostrom, University of Sussex, UK
Term graph rewriting for implementing the λ-calculus refactored
We retrace some history of using term graphs
for implementing β-reduction in the λ-calculus.
We refactor the following three high-lights from that
history, illustrated by a prototype implementation:
- the classical (first) term graph implementation (Wadsworth),
of β-reduction which we refactor through a term graph implementation
IMP of a well-behaved (e.g., orthogonal) class of TRSs;
- implementing β-reduction through repeated weak-reduction
(De Bruijn (Automath), Peyton Jones, Coquand, Grégoire & Leroy, Balabonski,...),
which we show can be performed on IMP;
- implementing needed β-reduction (Huet & Lévy, Barendregt, Kennaway, Klop, Sleep,...)
through a strategy for IMP that we dub α-spine. By making use of union-find techniques
for it, normal order reduction is shown to be linearly implementable.
Programme
Session 1
9:00 - 10:00 (Joint keynote with DIALOCO 2026)
Dan R. Ghica
(Huawei Central Software Institute & University of Birmingham, UK)
Syntactic trinitarianism: terms, graphs, diagrams
Coffee Break & Room Change
Session 2
10:30 - 11:30 (invited talk)
Nicolas Troquard
(Gran Sasso Science Institute, Italy)
Graph Neural Networks, Their Logics, and Formal Verification
11:30 - 12:00
Marc Thatcher
(University of Sussex, UK)
A Programming Language for Interaction Nets
(Extended Abstract)
12:00 - 12:30
Pedro Cunha, Sandra Alves and Mário Florido
(Faculdade de Ciˆencias da Universidade do Porto, Portugal)
Labels, paths and linearization of the λ -calculi
(Extended Abstract)
Lunch
Session 3
14:00 - 15:00 (invited talk)
Vincent van Oostrom
(University of Sussex, UK)
Term graph rewriting for implementing the λ-calculus refactored
15:00 - 15:30
Anna Matsui (Johns Hopkins University, USA)
and
Koko Muroya (Ochanomizu University, Japan)
Hypergraphs with Binding
(Extended Abstract)
Coffee Break
Session 4
16:00 - 16:30
Dale Miller
(Inria Saclay and LIX, Institut Polytechnique de Paris, France)
Relating ordered hypergraph rewriting and proof theory: Work in progress
(Extended Abstract)
16:30 - 17:00
Bastiaan Laarakker and Tobias Kappé
(LIACS, Leiden University, The Netherlands)
Reducible Graphs and Bisimilarity of 1-free Star Expressions
(Extended Abstract)
17:00 - 17:30
Clemens Grabmayer
(Gran Sasso Science Institute, Italy)
Towards a Characterisation of the Graph Structure of Process Interpretations of Regular Expressions
(Extended Abstract)
17:30 - closing
Program Committee
- Koko Muroya, Ochanomizu University, Japan (co-chair)
- Kazunori Ueda, Waseda University, Japan (co-chair)
- Sandra Alves, University of Porto, Portugal
- Clemens Grabmayer, Gran Sasso Science Institute, Italy
- Amar Hadzihasanovic, Tallinn University of Technology, Estonia
- Makoto Hamana, Kyushu Institute of Technology, Japan
- Jens Kosiol, Philipps-Universität Marburg, Germany
- Robin Piedeleu, University College London, UK
- Chris Poskitt, Singapore Management University, Singapore
- Femke van Raamsdonk, Vrije Universiteit Amsterdam, Netherlands
- Michele Sevegnani, University of Glasgow, UK
Contact: Kazunori
Ueda / Last modified: July 17, 2026