ABSTRACT. 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.

ABSTRACT. We study how to embed well-known hypergraph grammars based on the double pushout (DPO) approach in the hypergraph Lambek calculus HL. It turns out that DPO rules can be naturally encoded by types of HL. However, this encoding is not enough to convert a DPO grammar into an equivalent grammar based on HL: we additionally need a logical operation that would allow making arbitrarily many copies of types. We develop such an operation called the conjunctive Kleene star and show that any DPO grammar can be converted into an equivalent HL-grammar enriched with this operation.

ABSTRACT. We show a proof term in a string rewrite system can be mapped to its causal graph and that the latter is a unique representative of the permutation equivalence class of the former. We then map the causal graph back to a proof term of a special shape, a so-called greedy multistep reduction. Composing both transformations yields a simple and effective way of constructing the greedy multistep reduction of a proof term, and thereby of deciding permutation equivalence of proof terms in general, and of (multistep) reductions in particular.

ABSTRACT. 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.

ABSTRACT. We will give an overview of various results on graph rewriting with PBPO+. PBPO+ is a versatile graph rewriting formalism based in category theory that subsumes many well-known approaches such as DPO, SqPO and AGREE (at least in the setting of quasitopoi).

ABSTRACT. The BPMN is a widely used standard notation for defining intra- and inter-organizational workflows. However, the informal description of the BPMN execution semantics leads to different interpretations of BPMN constructs and difficulties in checking behavioral properties. Other approaches to formalizing BPMN’s execution semantics only partially cover BPMN. To this end, we propose a formalization that, compared to other approaches, covers most of the BPMN constructs. Our approach is based on a model transformation from BPMN models to graph grammars. As a proof of concept, we have implemented our approach in an open-source web-based tool.

ABSTRACT. We introduce Ideograph, a language for expressing and manipulating structured data. Its types describe kinds of structures, such as natural numbers, lists, multisets, binary trees, syntax trees with variable binding, directed acyclic graphs, and relational databases. Fully normalized terms of a type correspond exactly to members of the corresponding structure, analogous to a Church encoding. Non-normal terms encode alternate representations of their fully normalized forms. In this paper, we first illustrate the correspondence between terms in our language and standard Church encodings, and then we exhibit the type of closed terms in untyped lambda calculus.