IWS on Friday, July 9th

09:00‑10:00 Invited talk
Location: IF 1.16
09:00 Dan Dougherty (Worcester Polytechnic Institute, USA)
Game Strategies and Rule-Based Systems

The classical notion of term-rewriting strategy has in recent years been expanded to find application in a wide variety of rule-based computing scenarios, including proof-search, program transformation, and planning. In parallel with these developments, games played on graphs have been extensively studied in the verification community, with game strategies as a central notion. It is natural to wonder whether the use of the term "strategy" in both of these two contexts is more than a pun. In this talk we explore some consequences of viewing strategies in rule-based systems as strategies in games, specifically sequential games of perfect information. In a foundational vein, viewing rewriting strategies as game strategies suggest a new approach to the semantics of rewriting strategies. As a second application we describe how certain security policies can be profitably viewed as strategies, and report on nascent work on policy synthesis via game-solving.

10:30‑12:30 Regular talks
Location: IF 1.16
10:30 Alvaro Garcia, Pablo Nogueira and Emilio Jesus Gallego Arias
The Beta Cube

We define a template for big-step-style reduction strategies that can be instantiated to the foremost (and more) reduction strategies of the pure lambda calculus. We implement the template in Haskell as a parametric reducer whose fixed points are reduction strategies. The resulting code is clean and abstracts away from the machinery required to guarantee semantics preservation for all strategies in lazy Haskell. By interpreting some parameters as boolean switches we obtain a reduction strategy lattice or beta cube which captures the strategy space neatly and systematically. We define a hybridisation operation that generates hybrid strategies by composing a base and a subsidiary strategy from the cube. We prove an absorption theorem which states that subsidiaries are left-identities of their hybrids. More properties from the cube remain to be explored.

11:00 Alex Gerdes, Bastiaan Heeren and Johan Jeuring
Properties of Exercise Strategies

Mathematical learning environments give domain-specific and immediate feedback to students solving a mathematical exercise. We have developed a feedback framework based on a strategy language that automatically calculates semantically rich feedback. We offer this feedback functionality to mathematical environments via a set of web services. Feedback is only effective when it is precise and to the point. The tests we have performed give some confidence about the correctness of our feedback services, but we want to formally specify, and, if possible, prove the properties our feedback services should satisfy. To give such a formalisation, we need a formal description of the concepts used in our services. In this extended abstract we give a formal definition of the concepts we use in our feedback framework. The formal and precise definition validates our implementation and makes it possible to reason about the concepts used. In addition, we give a number of desired properties that the concepts should have.

11:30 Bernhard Gramlich and Felix Schernhammer
Termination of Rewriting with - and Automated Synthesis of - Forbidden Patterns

We propose a method for the automated analysis of termination of term rewriting with forbidden patterns. This method is based on the well-known dependency pair framework using a modified version of dependency pairs called contextual dep- endency pairs. We present a DP processor exploiting the additional contextual information these modified dependency pairs provide. Finally we show that our approach can be used to automatically synthesize suitable forbidden patterns for a rewrite systems by generating them on the fly during the termination analysis.

12:00 Olivier Namet and Maribel Fernández
A strategy language for graph rewriting systems

We design a language that can be used to control the application of graph rewriting rules. The traditional operators found in strategy languages for term rewriting have been adapted to deal with the more general setting of graph rewriting, and some new constructs have been included to deal with graph traversal and management of rewriting positions in the graph. This language is part of a graph transformation environment that is currently being built within the PORGY project.

14:00‑15:00 Invited talk
Location: IF 1.16
14:00 Assia Mahboubi (INRIA, France)
Organizing and using algebraic structures in large developments of formalized mathematics

The Mathematical Component project, at the Inria Microsoft Research Joint Centre, investigates how to design large and consistent bodies of formalized mathematics. The playground of these investigations is a formalization in the Coq system of a finite group theory famous result: the proof of the Feit-Thompson theorem (1962), so called the Odd Order theorem. This milestone of the classification of finite simple groups is also by its length a historic publication in the story of mathematical literature. From a formal point of view, this proof is a true challenge. Some difficulties are well-known pitfalls of formal mathematics: set-theoretic versus type-theoretic definitions, catching the implicit content of mathematical texts,... But this proof also has the particularity of relying on a wide variety of elementary algebraic structures and theories: while local analysis has a combinatoric flavor, character theory requires a full formalization of standard linear algebra, field extensions, Galois theory... Beside the required background in group theory, half of the local analysis part of the proof is now formalized, plus standard linear algebra and some elementary module theory. In this talk, we will try to abstract from the specificities of the Feit-Thompson proof. We will review how the Coq system, and in particular both its computational features and its type inference mechanisms proves a precious and efficient tool in solving these compositionality and automation general issues.

15:30‑16:00 Regular talks (cont'd)
Location: IF 1.16
15:30 René Thiemann, Jürgen Giesl, Peter Schneider-Kamp and Christian Sternagel
Loops under Strategies ... Continued

Disproving termination of term rewrite systems is often done by giving an infinite reduction in form of a finite looping reduction. Whereas for rewriting without strategies every loop indeed corresponds to an infinite reduction, this is not necessarily the case in presence of strategies. To this end, decision procedures have been developed which decide for a given loop whether it respects the innermost- our outermost strategy. In this paper we build upon these results and present new decision procedures for the strategies leftmost-innermost, leftmost-outermost, parallel-innermost, parallel-outermost, max-parallel-innermost, and max-parallel-outermost.

16:00‑17:00 Works in progress
Location: IF 1.16
16:00 Pascal Fradet, Jean-Louis Giavitto and Marnes Hoff
Refinement of Chemical Programs using Strategies

We sketch an approach where the basic functionality of a program is expressed as high level rules without artificial constraints on data structures or the control of execution. The programmer addresses efficiency issues separately in a second stage by specifying three implementation aspects: the data structure, the selection of elements and the evaluation strategy. These aspects are used to refine the source program and automatically generate a low-level efficient program. We focus on the refinement of control using strategies and present the main ideas on simple examples.

16:20 Ian Mackie
Closed cut-elimination in linear logic

Closed cut-elimination is a specific strategy to eliminate some of the cuts in proofs, and for the purpose of this paper we focus on linear logic proofs. We give the sequent calculus and proof net formalism for this strategy, and an implementation of it as a system of interaction nets. The results can be applied to other logics of course through translation, but we only hint at these applications in the present paper.

16:40 Detlef PLUMP
Graph Programs

This paper gives a brief introduction to GP (for Graph Programs), an experimental nondeterministic programming language for high-level problem solving in the domain of graphs. The language is based on conditional rule schemata for graph transformation and thereby frees programmers from handling low-level data structures for graphs. The prototype implementation of GP compiles graph programs into bytecode for the York abstract machine, and comes with a graphical editor for programs and graphs.