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, 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), and online (2020, planned to be held in Paris).The permanent TERMGRAPH website has further information.
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):
Papers will be judged on relevance, originality, correctness, and usefulness. Preliminary proceedings will be available for the workshop.
After the workshop, authors will be invited to submit a longer version of their work (a 15-pages 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:
We provide a tutorial introduction to the algebraic graph rewriting formalism PBPO+. We show how PBPO+ can be obtained by composing a few simple building blocks. Along the way, we comment on how alternative design decisions lead to related formalisms in the literature, such as DPO.
In this talk we will present a computational interpretation of Girard's proof nets for intuitionistic linear logic. More precisely, proof nets are a graphical formalism representing bureaucracy-free proofs, i.e., the order in which independent logical rules are applied in a derivation is abstracted. Despite the obvious advantage of the graphical notation, the essence of their corresponding operational semantics is not always clear from a programming point of view, and a term syntax often provides a complementary understanding of a (bureaucracy-free) graph framework.
Our goal is to define a new term language that establishes a faithful and fine-grained Curry-Howard correspondence with Girard's intuitionistic NP, both from a static (objects) and a dynamic (reductions) point of view. On the static side, we identify an equivalence relation on terms which is sound and complete with respect to the classical notion of structural equivalence for proof-nets. On the dynamic side, we show that every single (exponential) step in the term calculus translates to a different single (exponential) step in the graphical formalism, thus capturing the original Girard’s granularity of proof-nets but on the level of terms.
Registration to the workshop will be possible via the FLoC registration page.
Last modified: Tue May 09:40:01 UTC 2022 by clegra