WRS

WRS  Invited talks
List of invited speakers of WRS:
IWS 2012
A rewriting point of view on strategies

Hélène Kirchner
(INRIA France)

Strategies frequently occur in automated deduction and reasoning systems and more generally
are used to express complex designs for control in modeling, proof search, program
transformation, SAT solving or security policies. In these domains, deterministic rulebased
computations or deductions are often not sucient to capture complex computation or proof
development. A formal mechanism is needed, for instance, to sequentialize the search for
dierent solutions, to check context conditions, to request user input to instantiate variables,
to process subgoals in a particular order, etc. This is the place where the notion of
strategy comes in. In the communities of logic, verification and rewriting, definitions have
been given and progress has been made towards a deeper understanding of the nature of
strategies, their descriptions, their properties, and their usage.
Since the field is quite large, I will adopt in this talk the specific point of view of
rewriting. Rewriting logic and rewriting calculus are powerful formalisms to
express and study uniformly computations and deductions in automated deduction and
reasoning systems.
Based on rewriting concepts, several definitions of strategy will be reviewed and connected.
In order to catch the higherorder nature of strategies, a strategy is defined as a proof
term expressed in the rewriting calculus. To address in a coherent way deduction and
computation, a strategy is seen as a set of paths in a derivation tree whose reduction relation
is a onestep reduction. To recover the definition of strategy in sequential pathbuilding
games or in functional programs, a strategy is considered as a partial function that associates
to a reductioninprogress, the possible next steps in the reduction sequence.
The second part of the talk will address the specification of strategies by reviewing
several strategy languages that have been recently designed and studied on structures
like trees and graphs. Used for a long time in lambdacalculus, strategies are present in
programming languages such as Clean, Curry and Haskell, and can be explicitely defined
to rewrite terms in languages such as Elan, Stratego, Maude or Tom. They
are also present in graph transformation tools such as GP and PORGY. Based on
some of these approaches, we will identify useful constructs that are necessary to express
control on rules and structures.

Refinements and Search Strategies for Semantic
Tableaux with Blocking

Renate Schmidt
(The University of Manchester, UK)

A popular approach to developing decision procedures for nonclassical logics including modal,
hybrid and description logics are ground semantic tableau calculi. Rules of ground semantic
tableau calculi perform inference steps in a way that closely follows the semantics of a logic.
This property means tableau derivations are easy to understand and easy to construct both by
hand and automatically.
Another reason for the popularity of ground semantic tableau calculi is the ease with which
they can be devised for semantically defined logics. We recently developed a tableau synthesis
framework, which shows that it is in fact possible to obtain sound and complete calculi semi
automatically from the specification of the semantics of a logic. There are also effective and
general ways to obtain terminating tableau calculi. For example, adding the unrestricted blocking
mechanism to sound and complete ground semantic calculus gives a terminating calculus
for the logic, when the logic has the finite model property.
Because the rules of a tableau calculus provide the basis for a nondeterministic deduction procedure,
there is essentially complete flexibility in how tableau derivations may be constructed.
In particular, the calculus does not give instructions of which branch to select for
expansion, it does not tell which rule to apply next and does not specify which of many possible
formulae to apply a rule to or which of many terms to use for instantiation. This means
the search space is generally huge. There are however standard principles for containing the
search space and tackling the challenges of obtaining effective implementations while inheriting
soundness, completeness and termination from the tableau calculus.
In this talk we are particularly interested in ways of making it easier to achieve an efficient
implementation of a tableau calculus. We emphasise techniques to refine tableau calculi, rule
simplification and redundancy, and in general principles to develop more effective tableau
calculi. We discuss ways of dealing with the various forms of nondeterminism, including efficient
and fair application of rules with universal extent. Particularly challenging is the realisation of
blocking mechanisms to obtain decision procedures.

WRS 2011
The Maude strategy language and some of its
applications

Narciso MartíOliet
(U. Complutense, Spain)

Maude is a declarative specification and programming language based on rewriting logic.
A Maude rewrite theory essentially consists of a signature, a set of equations, and a set
of (conditional) rewrite rules. While the set of equations is assumed to be confluent and
terminating, so that every term has a normal form with respect to equational reduction,
rewrite rules can be nonconfluent or nonterminating.
A strategy is described as an operation that, when applied to a given term, produces a set
of terms as a result, given that the process is nondeterministic in general. The basic strategies
consist of the application of a rule to a given term, but rules can be conditional with respect
to some rewrite conditions which in turn can also be controlled by means of strategies. Those
basic strategies are combined by means of several combinators, including: regular expression
constructions (concatenation, union, and iteration), ifthenelse, combinators to control the
way subterms of a given term are rewritten, and recursion. Furthermore, strategies can also
be generic.
This strategy language has been endowed with both a simple settheoretic semantics and
a rewriting semantics, which are sound and complete with respect to the controlled rewrites.
Moreover, the rewriting semantics also enjoys properties of monotonicity and persistence.
The first applications of the strategy language included the operational semantics of
process algebras such as CCS and the ambient calculus. The same ideas were later applied
to the twolevel operational semantics of the parallel functional programming language Eden
and to modular structural operational semantics. It has also been used in the implementation
of basic KnuthBendix completion algorithms and of congruence closure algorithms. Other
applications include a sudoku solver, neural networks, membrane systems, hierarchical design
graphs, and a representation of BPMN.

Graph Programs: Semantics, Verification and Implementation

Detlef Plump
(University of York, UK)

GP is a rulebased, nondeterministic programming language for highlevel problem solving
in the domain of graphs, freeing programmers from handling lowlevel data structures. The
language has a simple syntax and semantics, to facilitate formal reasoning about programs.
In this talk, I will introduce GP by a number of example programs and discuss its structural
operational semantics. A special feature of this semantics is the use of failing computations to
de ne branching and iteration. I will then present proof rules for Hoarestyle veri cation of
graph programs, and demonstrate their use by verifying a simple colouring program. Finally,
I will brie
y describe GP's current implementation.

IWS 2010
Game Strategies and RuleBased Systems/font>

Dan Dougherty
(Worcester Polytechnic Institute, USA)

The classical notion of termrewriting strategy has in recent years been expanded to find application
in a wide variety of rulebased computing scenarios, including proofsearch, 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 rulebased 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 gamesolving.
The talk will touch on ongoing projects that are joint work with Emilie Balland, Joshua Guttman,
Claude Kirchner, and Hélène Kirchner.

Organizing and Using Algebraic Structures in Large
Developments of Formalized Mathematics

Assia Mahboubi
(INRIA, France)

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
FeitThompson 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 wellknown pitfalls
of formal mathematics: settheoretic versus typetheoretic 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 FeitThompson 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.

WRS 2009
From Abstract Strategies to Strategic Rewriting

Hélène Kirchner
(INRIA Bordeaux, France)

Strategies are ubiquitous in automated deduction and reasoning
systems, yet only since about ten years have they been studied
in their own right. In the two communities of automated deduction and
rewriting, workshops have been launched to make progress towards a
deeper understanding of the nature of strategies, their descriptions, their
properties, and their usage. Recently strategies have come to be viewed
more generally as expressing complex designs for control in modeling,
proof search, program transformation, and access control.
In this talk, we are contributing to the theoretical foundations of strategies.
We first present a general definition of abstract strategies that allows
the convergence of different points of view, namely rewritingbased computations
on one hand, rulebased deduction and proofsearch on the
other hand. This definition is extensional in the sense that a strategy
is taken there explicitly to be a set of paths of an abstract reduction
system. We then move to a more intensional definition compliant with
the abstract view but more operational in the sense that it describes a
means for determining such a set. This naturally leads to define strategic
reductions and their instances on terms, namely strategic rewritings.
We rely on previous works that are briefly described and on strategy
languages that have been recently designed and studied.

Programming with nondeterministic functions:
some rewriting and semantic issues

Francisco LópezFraguas
(U. Complutense, Spain)

Nondeterministic functions are a nice programming construct
that can compete in elegance, conciseness and even efficiency
with other highlevel approaches to nondeterminism, like the use of relations
in logic programming. Nonconfluent constructorbased rewrite
systems are a very adequate formalism giving syntactic support to nondeterministic
functions. However, there are different options about the
kind of nondeterminism to be realized, a major distinction being that
of runtime choice and calltime choice.
In this talk we revise some recent (and not so recent) advances in relation
to the description of different variants of nondeterminism (and their
combination), at the operational level by giving formal definitions of
the reduction process and at the semantic level by giving logical calculi
prescribing the possible results of computations.

WRS 2008
Diagram Rewriting: Examples and Theory

Yves Lafont
(U. de la Méditerranée, France)

Diagrams are a natural 2dimensional generalization of words. They are
used in many areas of mathematics, physics, and computer science. I
will present some fundamental examples of diagram rewriting, leading
to an algebraic theory of boolean circuits.

WRS 2007
On TermGraph Rewrite Strategies

Rachid Echahed
(IMAG Grenoble, France)

Graph rewriting is being investigated in various areas nowadays.
In this talk, we consider termgraph rewriting as the underlying
operational semantics of rulebased (functional or logic)
programming languages

Rules and Strategies in Java

PierreEtienne Moreau
(INRIA and LORIA Nancy, France)

In this talk we present the essential feature we have considered when
designing a new language based on rules and strategies.
Relying on the implementation of Tom, we explain how these ingredients can
be implemented and integrated in a Java environment.

WRS 2006
Programmed Strategies for Program Verification

Richard Kieburtz
(OGI Portland, OR, USA)

Plover is an automated propertyverifier for Haskell programs that has been under
development for the past three years as a component of the Programatica
project. In Programatica, predicate definitions and property assertions written
in Plogic, a programming logic for Haskell, can be embedded in the text of a
Haskell program module. Plogic properties refine the type system of Haskell
but cannot be verified by typechecking alone; a more powerful logical verifier is
needed. Plover codes the proof rules of Plogic, and additionally, embeds strategies
and decision procedures for their application and discharge. It integrates a
reduction system that implements a rewriting semantics for Haskell terms with a
congruenceclosure algorithm that supports reasoning with equality. It can employ
splitting strategies to explore alternative valuations of expressions of type
Bool or other finite data types, but these strategies lead to exponential growth
of terms and must be employed cautiously. Plover itself is written in Stratego,
which has proven to be a powerful language in which to write a verifier. This talk
will explain the design and implementation of some of the strategies that enable
Plover to comprehend Haskell and to discharge some valid property assertions.

Rewriting (your) Calculus

Claude Kirchner
(INRIA and LORIA Nancy, France)

Rewriting is clearly established as a general paradigm which agility eases to
express and reason about computation and deduction. The rewriting calculus,
generalizing the lambda calculus and the rewriting relation, provides us with a
theoretical and uniform foundation for this expressivity. Introduced in the late
nineties, the framework and its metaproperties are now better understood. We
will show why the calculus is wellsuited to represent computation as well as
deduction, and therefore deduction modulo.
The rewriting calculus is therefore a good candidate to backup proof assistants
where the user can adapt the computation mechanism to its needs. But
furthermore, we want the next generation of proof assistants to provide the user
with the possibility to adapt also the deduction system to its needs. We will see
how this could be designed and how it can be used to get better higherlevel
logical representation of userdefined theories.

WRS 2005
Implementing an evaluator for miniML in ATS: a case study of
combining programming with theorem proving

Hongwei Xi
(Boston, USA)


WRS 2004
Normalization by Evaluation

Olivier Danvy
(University of Aarhus, Denmark)


Reduction cycles

Jan Willem Klop
(Vrije Universiteit Amsterdam, The Netherlands)


WRS 2003
Strategies and User Interfaces in Maude

Manuel Clavel
(Universidad Complutense de Madrid, Spain)

Maude is a highlevel language and a highperformance system supporting
executable specification and declarative programming in rewriting logic.
Rewriting logic is reflective, in the sense of being able to express
its own metalevel at the object level. Reflection is systematically
exploited in Maude endowing the language with powerful metaprogramming
capabilities. We explain and illustrate with examples two of
these reflective features: userdefinable declarative strategies and userdefinable
declarative interfaces. We conclude with an application, namely, an
inductive theorem prover, whose implementation effectively combines
both reflective features.

Rewrite Strategies in the Rewriting Calculus

Claude Kirchner (LORIA  INRIA Lorraine, France)

This talk presents an overview on the use of the rewriting
calculus to express rewrite strategies. We motivate first the use
of rewrite strategies by examples in the ELAN language. We
then show how this has be modelled in the initial version of the
rewriting calculus and how the matching power of this
framework facilitates the writing of powerful strategies.

WRS 2002
Approximations for Strategies and Termination

Aart Middeldorp
(Tsukuba University, Japan)

In the talk we illustrate the use of approximations and tree
automata techniques to define optimal normalizing strategies
for large classes of firstorder rewrite systems. We further
show how the very same ideas can be used to improve the
dependency pair method for proving termination of rewrite
systems automatically. If time permits, we present a new and
computationally less expensive improvement for the latter.

Optimal Strategies in HigherOrder Rewriting

Vincent van Oostrom (Univ. of Utrecht, The Netherlands)

In a socalled optimal implementation of a term rewriting system,
only needed redexes are contracted and all redexpatterns in a term
which have the same history along the reduction,
are kept shared in the graph implementation of the term.
Such an implementation crucially relies on the notion of
`being the same along a reduction' of redexpatterns
in particular, and of parts of terms in general.
Lévy gave three ways to characterize this notion of sameness,
in the case of the lambdacalculus. Via:
 Labelling
 Extraction
 Zigzag
We are performing a similar program for leftlinear
(first and higherorder) term rewriting systems.
This requires general notions of, among others,
permutation equivalence, labelling, residuals, and tracing.
We present and relate these for the case of term rewriting,
all based on the technical tool of proof terms
(witnessing proofs in Meseguer's rewriting logic).
We conclude by presenting an extension of the
lambdacalculus with an endofscope operator,
which came up naturally, while extending the optimal
firstorder setting to higherorder.
The rough idea is that a role of the lambda is
to open a scope and it is only natural to introduce
an explicit operator to end a scope.
The nice thing is that (an extension of)
betareduction can be defined which is confluent
without alphareduction. Alpha reduction is
only needed when removing endofscopes.
(This calculus is halfway toward an optimal implementation of
the lambda calculus: for that also the explicit operators
for (un)sharing, the socalled fanin and fanout,
need to be introduced.)
The first part of the talk is based on Chapter 8, joint work with
Roel de Vrijer,
of the forthcoming book on
Term Rewriting Systems, by Terese.
The second part of the talk on the lambda calculus with scopes,
is based on joint work (in progress) with
Dimitri Hendriks
who's also working on a
formalization in Coq.
The extension to higherorder is joint workinprogress
with Sander Bruggink.

WRS 2001
Evaluation Strategies for Functional Logic Programming

Sergio Antoy
(Portland State University, USA)

Recent advances in the foundations and the development of functional
logic programming languages originate from farreaching results on narrowing
evaluation strategies. Narrowing is a computation similar to rewriting
which yields substitutions in addition to normal forms. In functional logic programming,
the classes of rewrite systems to which narrowing is applied are, for
the most part, subclasses of the constructorbased, possibly conditional, rewrite
systems. Many interesting narrowing strategies, particularly for the smallest subclasses
of the constructorbased rewrite systems, are generalizations of wellknown
rewrite strategies. However, some strategies for larger nonconfluent subclasses
have been developed just for functional logic computations. In this paper,
I will discuss the elements that play a relevant role in evaluation strategies for
functional logic programming, describe some important classes of rewrite systems
that model functional logic programs, show examples of the differences in
expressiveness provided by these classes, and review the characteristics of narrowing
strategies proposed for each class of rewrite systems.

Slides

A Survey of Strategies in Program Transformation Systems

Eelco Visser (Univ. of Utrecht, The Netherlands)

Program transformation is used in a wide range of applications including compiler
construction, optimization, program synthesis, refactoring, software renovation, and
reverse engineering. Complex program transformations are achieved through a number
of consecutive modifications of a program. Transformation rules define basic
modifications. A transformation strategy is an algorithm for choosing a path in
the rewrite relation induced by a set of rules. This paper surveys the support for
the definition of strategies in program transformation systems. After a discussion
of kinds of program transformation and choices in program representation, the basic
elements of a strategy system are discussed and the choices in the design of a
strategy language are considered. Several styles of strategy systems as provided in
existing languages are then analyzed.

