View: session overviewtalk overviewside by side with other conferences

08:30-09:00Coffee & Refreshments
09:00-10:30 Session 26J

Invited Talk by Delia Kesner

Location: Ullmann 101
A Computational Interpretation of Girard’s Intuitionistic Proof-Nets

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.

10:30-11:00Coffee Break
11:00-12:30 Session 31N

Regular submissions, morning session

Location: Ullmann 101
Transformation of DPO Grammars into Hypergraph Lambek Grammars With The Conjunctive Kleene Star

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.

Greedily Decomposing Proof Terms for String Rewriting into Multistep Derivations by Topological Multisorting

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.

A PBPO+ Graph Rewriting Tutorial
PRESENTER: Roy Overbeek

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.

12:30-14:00Lunch Break

Lunches will be held in Taub hall and in The Grand Water Research Institute.

14:00-15:30 Session 34N

Invited talk by Jörg Endrullis

Location: Ullmann 101
PBPO+ Graph Rewriting in Context

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

15:30-16:00Coffee Break
16:00-17:30 Session 37M

Regular papers, afternoon session, including discussion

Location: Ullmann 101
Formalization and analysis of BPMN using graph transformation systems
PRESENTER: Tim Kräuter

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.

Ideograph: A Language for Expressing and Manipulating Structured Data
PRESENTER: Stephen Mell

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.

18:30-20:00Workshop Dinner (at the Technion, Taub Terrace Floor 2) - Paid event