View: session overviewtalk overviewside by side with other conferences

09:15-10:15 Session 24A: Joint DCM / TermGraph Invited Talk (joint with DCM)
Location: FH, Seminarraum 325/2
Numeral Systems in the Lambda Calculus
SPEAKER: Ian Mackie

ABSTRACT. We investigate numeral systems in the λ-calculus; specifically
in the linear λ-calculus where copying and erasing are not
permitted. Our interest is in finding efficient (and where possible,
in constant time) representations for successor, predecessor,
addition, subtraction and test for zero.  We begin by recalling some
well-known systems, before going on to the linear case where we give
several systems with different properties. We conclude with a
characterisation of linear numeral systems.

10:15-10:45Coffee Break
10:45-12:15 Session 26F: Computing with Graphs
Location: FH, Seminarraum 325/2
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.

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.

Nested Term Graphs

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.

13:00-14:30Lunch Break
14:30-15:30 Session 31D: Joint IWC / TermGraph Invited Talk (joint with IWC)
Location: FH, Seminarraum 325/2
An Introduction to Higher-Dimensional Rewriting Theory
SPEAKER: Samuel Mimram
15:30-16:00 Session 33F: Proof Nets
Location: FH, Seminarraum 325/2
Injectivity of Relational Semantics for (Connected) MELL Proof-Nets via Taylor Expansion

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:00-16:30Coffee Break
16:30-17:30 Session 34E: Implementations
Location: FH, Seminarraum 325/2
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.

Fixed Point Theory for Consistent Rewriting in Logic of Action with Reverse

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.