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 rule-based 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 di erent 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 higher-order 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 one-step reduction. To recover the definition of strategy in sequential path-building games or in functional programs, a strategy is considered as a partial function that associates to a reduction-in-progress, 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 lambda-calculus, 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 non-classical 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 non-deterministic 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 non-determinism, 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), if-then-else, 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 set-theoretic 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 two-level 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 Knuth-Bendix 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 rule-based, nondeterministic programming language for high-level problem solving in the domain of graphs, freeing programmers from handling low-level 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 Hoare-style 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 Rule-Based Systems/font>
Dan Dougherty (Worcester Polytechnic Institute, USA)

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

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 rewriting-based computations on one hand, rule-based deduction and proof-search 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 non-deterministic functions: some rewriting and semantic issues
Francisco López-Fraguas (U. Complutense, Spain)

Non-deterministic functions are a nice programming construct that can compete in elegance, conciseness and even efficiency with other high-level approaches to non-determinism, like the use of relations in logic programming. Non-confluent constructor-based rewrite systems are a very adequate formalism giving syntactic support to nondeterministic functions. However, there are different options about the kind of non-determinism to be realized, a major distinction being that of run-time choice and call-time choice. In this talk we revise some recent (and not so recent) advances in relation to the description of different variants of non-determinism (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 2-dimensional 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 Term-Graph Rewrite Strategies
Rachid Echahed (IMAG Grenoble, France)

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

Rules and Strategies in Java
Pierre-Etienne 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 property-verifier 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 P-logic, a programming logic for Haskell, can be embedded in the text of a Haskell program module. P-logic properties refine the type system of Haskell but cannot be verified by type-checking alone; a more powerful logical verifier is needed. Plover codes the proof rules of P-logic, 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 congruence-closure 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 meta-properties are now better understood. We will show why the calculus is well-suited 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 higher-level logical representation of user-defined theories.

WRS 2005

Proof Score Method in CafeOBJ
Kokichi Futatsugi (JAIST, Japan)

Implementing an evaluator for mini-ML 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 high-level language and a high-performance 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: user-definable declarative strategies and user-definable 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 first-order 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 Higher-Order Rewriting
Vincent van Oostrom (Univ. of Utrecht, The Netherlands)

In a so-called optimal implementation of a term rewriting system, only needed redexes are contracted and all redex-patterns 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 redex-patterns 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 lambda-calculus. Via:

  • Labelling
  • Extraction
  • Zig-zag
We are performing a similar program for left-linear (first- and higher-order) 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 lambda-calculus with an end-of-scope operator, which came up naturally, while extending the optimal first-order setting to higher-order. 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) beta-reduction can be defined which is confluent without alpha-reduction. Alpha reduction is only needed when removing end-of-scopes. (This calculus is halfway toward an optimal implementation of the lambda calculus: for that also the explicit operators for (un)sharing, the so-called fan-in and fan-out, 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 higher-order is joint work-in-progress 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 far-reaching 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 constructor-based, possibly conditional, rewrite systems. Many interesting narrowing strategies, particularly for the smallest subclasses of the constructor-based rewrite systems, are generalizations of well-known rewrite strategies. However, some strategies for larger non-confluent 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.


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.

Last update July 2005 # slucas@dsic.upv.es