WRS on Friday, August 11th

Joint RULE/WRS Invited Talk (09:00‑10:00)
Location: Suite 2628

09:00‑10:00

Claude Kirchner (INRIA & LORIA, Nancy, France) Rewriting (your) Calculus [pdf]

Session 1 (10:00‑10:30)
Location: Suite 2828

10:00‑10:30

Naoki Nishida (Nagoya University) Tomohiro Mizutani (Nagoya University) Masahiko Sakai (Graduate School of Infomation Science, Nagoya University) Transformation for Refining Unraveled Conditional Term Rewriting Systems Unravelings, which transform conditional term rewriting systems (CTRSs) into (unconditional) term rewriting systems, are useful for analyzing properties of CTRSs and for simulating reduction sequences of CTRSs. To avoid undesired reduction sequences of the unraveled CTRSs, reductions by the unraveled CTRSs are imposed a particular context-sensitive and membership condition that depends on extra function symbols introduced by means of the unravelings. In this paper we give a method to reduce the restriction, that is, to reduce the number of extra symbols. As the first step, we simply improve the ordinary unraveling for deterministic CTRSs.As the second step, we propose a transformation that folds two rewrite rules used successively which satisfy some delicate condition, to a rewrite rule which simulates reduction by the two rules.

Break (10:30‑11:00)

Session 2: Programming Languages and Implementations (11:00‑12:30)
Location: Suite 2828

11:00‑11:30	Horatiu Cirstea (Loria) Germain Faure (LORIA) Maribel Fernández (King's College London) Ian Mackie (Ecole Polytechnique) Francois-Regis Sinot (Ecole Polytechnique) New Evaluation Strategies for Functional Languages We use the rho-calculus as an intermediate language to compile functional languages with pattern-matching features, and give an interaction net encoding of the rho-terms arising from the compilation. This encoding gives rise to new strategies of evaluation, where pattern-matching and `traditional' beta-reduction can proceed in parallel without additional overheads.
11:30‑12:00	Mercedes Hidalgo-Herrero (Universidad Complutense) Alberto Verdejo (Universidad Complutense) Yolanda Ortega-Mallen (Universidad Complutense) Using Maude and its strategies for analyzing Eden semantics Eden is a parallel extension of the functional language Haskell. On behalf of parallelism Eden overrides Haskell’s pure lazy approach, combining a non-strict functional application with eager process creation and eager communication. We desire to investigate alternative semantics for Eden in order to analyze the consequences of some of the decisions adopted during the language design. In this paper we show how to implement in Maude the operational semantics of Eden in such a way that semantic rules can be modified easily. Moreover, other semantic features can be implemented by modifying a set of parameters of the semantics but without modifying the semantic rules.
12:00‑12:30	Muck van Weerdenburg (Eindhoven University of Technology) An account of implementing applicative term rewriting Generation of labelled transitions systems from system specifications is highly dependent on efficient rewriting (or related techniques). We give an account of the implementation of two rewriters of the mCRL2 toolset and evaluate them by comparing them with other commonly used efficient rewriters.

Lunch break (12:30‑14:00)

Joint RULE/WRS Invited Talk (14:00‑15:00)
Location: Suite 2628

14:00‑15:00

Dick Kieburtz (OGI School of Science and Engineering, OHSU, Portland, Oregon) Programmed Strategies for Program Verification [ppt] 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.

Session 3 (15:00‑15:30)
Location: Suite 2828

15:00‑15:30

Claudio Sacerdoti Coen (University of Bologna) Reduction and conversion strategies for the Calculus of (co)Inductive Constructions: Part I We compare several reduction and conversion strategies for the Calculus of (co)Inductive Constructions by running benchmarks on the library of the Coq proof assistant. All the strategies have been implemented in an independent verifier for the proof objects of Coq that is part of the Matita proof assistant.

Break (15:30‑16:00)

Session 4: Application of Strategies (16:00‑17:00)
Location: Suite 2828

16:00‑16:30

Karl Trygve Kalleberg (University of Bergen) Eelco Visser (Universiteit Utrecht) Strategic Graph Rewriting Some transformations and many analyses on programs are either difficult or unnatural to express using terms. In particular, analyses that involve type contexts, call- or control flow graphs are not easily captured in term rewriting systems. In this paper, we describe an extension to the System S term rewriting system that adds references. We show how references are used for graph rewriting, how we can express more transformations with graph-like structures using only local matching, and how references give a representation that is more natural for structures that are inherently graph-like. Furthermore, we discuss tradeoffs of this extension, such as changed traversal termination and unexpected impact of reference rebinding.

16:30‑17:00

Sandra Alves (University of Porto) Maribel Fernández (King's College London) Mario Florido (University of Porto) Ian Mackie (Ecole Polytechnique) The Power of Closed Reduction Strategies Closed reduction is a strategy that has been used to provide new strategies of reduction in the lambda calculus: reductions can only take place when certain terms are closed (i.e. do not contain free variables). This has lead to various applications, such as a calculus of explicit substitutions, an alpha-conversion free calculus amongst other applications. In the first part of this paper we recall some of these applications. The main contribution of the paper is a new application of this strategy to a linear version of G\"odel's System T, where we show that closed reduction offers a huge increase in expressive power over the usual notion: which is closed by construction rather than closed by reduction.

Session 5: WRS Business Meeting (17:00‑17:30)
Location: Suite 2828