RDP                     
Home page
Organization
Sponsors

MEETINGS        
RTA
TLCA
FTP
WG1.6
RULE
UNIF
WFLP
WRS
WST

VENUE               
Valencia
Registration
Accomodation
Travelling
Program
Conference Venue
Internet
WRS'03
3rd International Workshop on Reduction Strategies in Rewriting and Programming
Valencia, Spain, June 8, 2003


ABSTRACTS OF REGULAR PAPERS ACCEPTED FOR PRESENTATION

    Weak Reduction and Garbage Collection in Interaction Nets
    Jorge Sousa Pinto (Universidade do Minho, Braga, Portugal)

    This paper presents an implementation device for the weak reduction of interaction nets to interface normal form. The results produced by running several benchmarks are given, suggesting that weak reduction greatly improves the performance of the interaction combinators-based implementation of the $\lambda$-calculus.

    Simulating Liveness by Reduction Strategies
    Jürgen Giesl (RWTH Aachen, Germany)
    Hans Zantema (Eindhoven University of Technology, The Netherlands)

    In this paper we define a general framework to handle liveness and related properties by appropriate reduction strategies in abstract reduction and term rewriting. Classically, reduction strategies in rewriting are used to simulate the evaluation process in programming languages. The aim of our work is to use reduction strategies to also study liveness questions which are of high importance in practice (e.g., in protocal verification for distributed processes). In particular, we show how the problem of verifying liveness properties is related to termination of term rewrite systems (TRSs). Using our results, techniques for proving termination of TRSs can be used to verify liveness properties.

    Innermost Reductions Find All Normal Forms on Right-Linear Terminating Overlay TRSs
    Masahiko Sakai (Nagoya University, Japan)
    Koji Okamoto (Nagoya University, Japan)
    Toshiki Sakabe (Nagoya University, Japan)

    A strategy of TRSs is said to be complete if all normal forms of a given term are reachable from the term. We show the innermost strategy is complete for terminating, right-linear and overlay TRSs. This strategy is fairly efficient to calculate all normal forms of a given term by searching reduction trees.

    Call-by-value, call-by-name, and strong normalization for the classical sequent calculus
    Stéphane Lengrand (ENS Lyon, France)

    We present a typed calculus $\lambda\xi$ isomorphic to the implicational fragment of the classical calculus LK. Reductions in LK eliminate the cut-rule by local rewriting steps, which correspond to the computation of explicit substitutions. This bridges the gap between Curien and Herbelin's $\bar{\lambda}\mu\bar{\mu}$-calculus and Urban's rewriting system for proofs. Encodings of one into the other are defined, and from them we derive the strong normalization of $\bar{\lambda}\mu\bar{\mu}$, as well as a denotational semantics of continuations for two strategies CBV and CBN that we have identified in Urban's rewriting system.

    A Rewriting Strategy for Protocol Verification (Extended Abstract)
    Monica Nesi (Università degli Studi di L'Aquila, Italy)
    Giuseppina Rucci (Università degli Studi di L'Aquila, Italy)
    Massimo Verdesca (Università degli Studi di L'Aquila, Italy)

    This paper presents a rewriting strategy for the analysis and verification of communication protocols. In a way similar to the approximation technique defined by Genet and Klay, a rewrite system R specifies the protocol and a tree automaton A describes the initial set of communication requests. Given a term t that represents a property to be proved, a rewriting strategy is defined that suitably expands and reduces t using the rules in R and the transitions in A to derive whether or not t is recognized by the intruder. This is done by simulating a completion process in a bottom-up manner starting from t and trying to derive a transition t -> q_f from critical pairs, where q_f is a final state of the tree automaton. The rewriting strategy is defined by means of a set of inference rules and used for reasoning about the authentication and secrecy properties of the Needham-Schroeder public-key protocol.

    Call-by-Need Reductions for Membership Conditional Term Rewriting Systems
    Mizuhito Ogawa (Japan Science and Technology Corporation, Tokyo, Japan)

    This paper proves that, for a membership conditional term rewriting system R, (1) a reducible term has a needed redex if R is nonoverlapping, and (2) whether a redex is nv-needed is decidable.

    An Abstract Concept of Optimal Implementation
    Zurab Khasidashvili (Intel, IDC, Haifa, Israel)
    John Glauert (School of Information Systems, UEA, Norwich, England)

    In previous works, we introduced \emph{Stable Deterministic Residual Structures} (SDRSs), Abstract Reduction Systems with an axiomatized residual relation which model orthogonal term and graph rewriting systems, and \emph{Deterministic Family Structures} (DFSs), which add an axiomatized notion of \emph{redex-family} to capture known \emph{sharing} concepts in the \lc\ and other orthogonal rewrite systems. In this paper, we introduce and study a concept of \emph{implementation} of DFSs. We show that for any DFS $\cal F$, its implementation ${\cal F}_I$ is a non-duplicating DFSs with zig-zag as the family relation, where zig-zag is simply the symmetric and transitive closure of the residual relation on redexes with histories. Further, we show that sharing is compositional: the sharing in a DFS $\calF$ can be decomposed into a weaker sharing $\calF'$ (such as zig-zag) and a sharing in the implementation $\calF'_I$ of $\calF'$ stronger than zig-zag. These results require study of the family relation in non-duplicating SDRSs. We show that zig-zag forms a family-relation in every non-duplicating SDRS, and that it is the only \emph{separable} family relation in such SDRSs.

                                                                                                                                                                                                               
Last update May 2003 # sescobar@dsic.upv.es