View: session overviewtalk overviewside by side with other conferences

09:15 | Numeral Systems in the Lambda Calculus SPEAKER: Ian Mackie ABSTRACT. We investigate numeral systems in the λ-calculus; specifically |

10:45 | Needed Computations Shortcutting Needed Steps SPEAKER: Sergio Antoy ABSTRACT. We define a compilation scheme for a constructor-based strongly-sequential graph rewriting system which shortcuts some needed steps. The object code is a constructor-based graph rewriting system as well that is normalizing for the original system when using an innermost strategy. Hence, the object code can be easily implemented by eager functions in a variety of programming languages. Then, we modify our object code in a way that avoids totally or partially the construction of the contracta of some needed steps of a computation. When computing normal forms in this way, both memory consumption and execution time are reduced compared to ordinary rewriting computations in the original system. |

11:15 | Proving Termination of Unfolding Graph Rewriting for General Safe Recursion SPEAKER: Naohi Eguchi ABSTRACT. We present a new termination proof and complexity analysis of unfolding graph rewriting which is a specific kind of infinite graph rewriting expressing the general form of safe recursion. We introduce a termination order over sequences of terms together with an interpretation of term graphs into sequences of terms. Unfolding graph rewrite rules expressing the general safe recursion can be embedded into the termination order by the interpretation, yielding the polynomial runtime complexity. |

11:45 | Nested Term Graphs SPEAKER: Clemens Grabmayer ABSTRACT. We report on work in progress on `nested term graphs' for formalizing higher-order terms (e.g. finite or infinite lambda-terms), including those expressing recursion (e.g. terms in the lambda-calculus with letrec). The idea is to represent the nested scope structure of a higher-order term by a nested structure of term graphs. Based on a signature that is partitioned into atomic and nested function symbols, we define nested term graphs both intensionally, as tree-like recursive graph specifications that associate nested symbols with usual term graphs, and extensionally, as enriched term graph structures. These definitions induce corresponding notions of bisimulation between nested term graphs. Our main result states that nested term graphs can be implemented faithfully by first-order term graphs. |

14:30 | An Introduction to Higher-Dimensional Rewriting Theory SPEAKER: Samuel Mimram |

15:30 | Injectivity of Relational Semantics for (Connected) MELL Proof-Nets via Taylor Expansion SPEAKER: Luc Pellissier ABSTRACT. We show that: (1) the Taylor expansion of a cut-free MELL proof-structure R with atomic axioms is the (most informative part of the) relational semantics of R; (2) every (connected) MELL proof-net is uniquely determined by the element of order 2 of its Taylor expansion; (3) the relational semantics is injective for (connected) MELL proof-nets. |

16:30 | An Implementation Model for Interaction Nets SPEAKER: Shinya Sato ABSTRACT. To study implementations and optimisations of interaction net systems we propose a calculus to allow us to reason about nets, a concrete data-structure that is in close correspondence with the calculus, and a low-level language to create and manipulate this data structure. These work together so that we can describe the compilation process for interaction nets, reason about the behaviours of the implementation, and study the efficiency and properties. |

17:00 | Fixed Point Theory for Consistent Rewriting in Logic of Action with Reverse SPEAKER: Susumu Yamasaki ABSTRACT. This paper studies an action structure to recursively derive actions by rewriting, where the action is abstract as in process algebra and has its reverse action. A representation method of action denotations with action defaults is given by fixed point theory, where the denotations are owing to coexistence of actions and their reverses. As the next method, the reverse action is thought of as multiplicative inverse in a semiring, which can be formed by algebraic compositions of action structures to primarily express sequences of actions with the action denotations. In both ways, consistency to classify each action and its reverse into different sorts is respected. |