FLoC '02 - WRS Sunday July 21st

WRS on Sunday

Detailed program
Sunday July 21st, 2002
See also the unified by-slot program

Sessions take place in auditorium 6 unless otherwise indicated.

08:45-09:00 Opening

Session 1

09:00-

10:00

Aart Middeldorp, U Tsukuba, Japan
Invited talk: Approximations for strategies and termination
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.

10:00-

10:30

Pierre Réty, U Orléans, France
Julie Vuotto, U Orléans, France
Regular sets of descendants by leftmost strategy
For a constructor-based rewrite system R, a regular set of ground terms E, and assuming some additional restrictions, we build a finite tree automaton that recognizes the descendants of E, i.e. the terms issued from E by rewriting, according to leftmost strategy.

Session 2

11:00-

11:30

Mark van den Brand, CWI Amsterdam, The Netherlands
Paul Klint, CWI Amsterdam, The Netherlands
Jurgen Vinju, CWI Amsterdam, The Netherlands
Term rewriting with type-safe traversal functions
Term rewriting is an appealing technique for performing program analysis and program transformation. Tree (term) traversal is frequently used but is not supported by standard term rewriting. In this paper, many-sorted first-order term rewriting is extended with automatic tree traversal by adding two primitive tree traversal strategies and complementing them with three types of traversals. These so-called traversal functions can be either top-down or bottom-up. They can be sort preserving, mapping to a single sort, or a combination of these two. Traversal functiona have a simple design, their application is type-safe in a first-order many-sorted setting and can be implemented efficiently. We describe the operational semantics of traversal functions and discuss applications.

11:30-

12:00

Ralf Laemmel, CWI Amsterdam, The Netherlands
The sketch of a polymorphic symphony
Functional strategies were previously defined as first-class generic functions which can traverse into terms while mixing uniform and type-specific behaviour. The first-class status is witnessed by a combinator style of generic programming. This symphony reconstructs functional strategies as an amalgamation of certain bits of parametric polymorphism, type case, polytypism, and overloading. We illustrate the expressivness and conciseness of this reconstruction by providing highly parameterized definitions of traversal schemes. The resulting style of generic programming is extremely lightweight and easy to use because it only involves two special combinators not yet present in standard functional programming. The reconstruction is geared towards Haskell, and it is supported by a generative tool YAGH - Yet Another Generic Haskell.

12:00-

12:30

Karina Olmos, Utrecht U, The Netherlands
Eelco Visser, Utrecht U, The Netherlands
Strategies for source-to-source constant propagation
Data-flow optimizations are usually implemented on low-level intermediate representations. This is not appropriate for source-to- source optimizations, which reconstruct a source level program after transformation. In this paper we show how constant propagation, a well known data-flow optimization problem, can be implemented on abstract syntax trees in Stratego, a rewriting system extended with programmable rewriting strategies for the control over the application of rules and dynamic rewrite rules for the propagation of information.

Joint invited speaker

Joint with HOR
Room: auditorium 5

14:00-

15:00

Vincent van Oostrom, Utrecht U, The Netherlands
Invited talk: Optimal strategies in higher-order rewriting

Session 3

15:00-

15:30

John Glauert, UEA Norwich, UK
Zurab Khasidashvili, Bar-Ilan U, Israel
An abstract Böhm-normalization
In this paper, we study normalization by neededness with respect to 'infinite results', such as Böhm-trees, in an abstract framework of Stable Deterministic Residual Structures (SDRS). We formalize the concept of 'infinite results' as suitable sets of infinite reductions, and prove an abstract infinitary normalization theorem with respect to such sets. We also give a sufficient and necessary condition for existence of minimal normalizing reductions.

Session 4

16:00-

16:30

Elvira Albert, Polytechnic U of Valencia, Spain
Michael Hanus, U Kiel, Germany
Frank Huch, U Kiel, Germany
Javier Oliver, Polytechnic U of Valencia, Spain
Germán Vidal, Polytechnic U of Valencia, Spain
Operational semantics for lazy functional logic programs
In this paper we define an operational semantics for lazy functional logic programs including notions like sharing, concurrency, non- determinism, etc. Such a semantic description is not only important to provide appropriate language definitions to reason about programs and check the correctness of implementations but it is also a basis to develop language-specific tools, like program tracers, profilers, optimizers, etc. First, we define a "big-step" semantics in natural style to relate expressions and their evaluated results. Since this semantics is not sufficient to cover concurrency, search strategies, or to reason about costs associated to particular computations, we also define a "small-step" operational semantics covering the features of modern functional logic languages. Finally, we provide the correctness of the small-step operational semantics.

16:30-

17:00

William L. Harrison, Oregon Health and Science U, USA
Richard B. Kieburtz, Oregon Health and Science U, USA
Pattern-driven reduction in Haskell
Haskell is a functional programming language with nominally non-strict semantics, implying that evaluation of a Haskell expression proceeds by demand-driven reduction. However, Haskell also provides pattern matching on arguments of functions, in let expressions and in the match clauses of case expressions. Pattern matching requires data- driven reduction to the extent necessary to evaluate a pattern match or to bind variables introduced in a pattern. In this paper, we provide both an abstract semantics and a logical characterization of pattern-matching in Haskell and the reduction order that it entails.

17:00-

17:30

Mauricio Ayala-Rincón, U Brasilia, Brazil
Rinaldi Maya Neto, U Brasilia, Brazil
Ricardo P. Jacobi, U Brasilia, Brazil
Carlos Llanos, IESB Brasilia, Brazil
Reiner Hartenstein, U Kaiserslautern, Germany
Applying ELAN strategies in simulation processors over simple architectures
Simulation of processors over simple architectures is an important technique for verifying previously to the expensive hardware implementation techniques involved in new technologies. Arvind's group has illustrated how to describe processors by reweriting and introduced a technique for proving the correctness of elaborated processors with respect to basic ones. The correctness of a processor is proved by showing that its related rewriting system does all that other rewriting system, considered correct, does. Basic concepts of rewriting as noetherianity and confluence are relevant for showing adequability of these rewrite based processor descriptions. In Arvind group's approach, simulation of the described is not done directly over the rewriting systems but over standard hardware description languages like Verilog after translating these rewrite descriptions adequately. Her we show how rewriting logic may be applied for purely rewriting simulation of processors and other proposals as is the case of evaluating performance of important hardware aspects of processors. Environments like ELAN, that is the one we use, are sufficiently versatile to allow for adequate implementations and easy modifications that are intrinsically related with hardware properties like the size and control of reorder buffers and the method of predictions used by speculative processors.pattern-matching in Haskell and the reduction order that it entails.