RTA on Tuesday

Detailed program
Tuesday July 23rd, 2002
See also the unified by-slot program

Sessions take place in auditorium 3 unless otherwise indicated.

Session 5

Chair: Femke van Raamsdonk

09:00-09:30  Paula Severi, U Turin, Italy
Fer-Jan de Vries, U Leicester, UK
An extensional Böhm model
We show the existence of an infinitary confluent and normalising extension of the finite extensional lambda calculus with beta and eta. Besides infinite beta reductions also infinite eta reductions are possible in this extension, and terms without head normal form can be reduced to bottom. As corollaries we obtain a simple, syntax based construction of an extensional Böhm model of the finite lambda calculus; and a simple, syntax based proof that two lambda terms have the same semantics in this model if and only if they have the same eta-Böhm tree if and only if they are observationally equivalent wrt to beta normal forms.
The confluence proof reduces confluence of beta, bottom and eta via infinitary commutation and postponement arguments to confluence of beta and bottom and confluence of eta.
We give counterexamples against confluence of similar extensions based on the identification of the terms without weak head normal form and the terms without top normal form (rootactive terms) respectively.

09:30-10:00  Julien Forest, U Paris XI (Paris-Sud), France
A weak calculus with explicit operators for pattern matching and substitution
In this paper we propose a Weak Lambda Calculus having explicit operators for Pattern Matching and Substitution. This formalism is able to specify functions defined by cases via pattern matching constructors as done by most modern functional programming languages such as OCAML. We show the main property enjoyed by this lambda calculus, namely subject reduction, confluence and strong normalization.

10:00-10:30  Chuck Liang, Hofstra U, USA
Gopalan Nadathur, U Minnesota, USA
Application paper: Tradeoffs in the intensional representation of lambda terms
Higher-order representations of objects such as programs, specifications and proofs are important to many metaprogramming and symbolic computation tasks. Systems that support such representations often depend on the implementation of an intensional view of the terms of suitable typed lambda calculi. Refined lambda calculus notations have been proposed that can be used in realizing such implementations. There are, however, choices in the actual deployment of such notations whose practical consequences are not well understood. Towards addressing this lacuna, the impact of three specific ideas is examined: the de Bruijn representation of bound variables, the explicit encoding of substitutions in terms and the annotation of terms to indicate their independence on external abstractions. Qualitative assessments are complemented by experiments over actual computations. The empirical study is based on λProlog programs executed using suitable variants of a low level, abstract machine based implementation of this language.

Session 6

Chair: Jürgen Giesl

11:00-12:00  John C. Mitchell, Stanford U, USA
Invited talk: Multiset rewriting and security protocol analysis
The Dolev-Yao model of security protocol analysis may be formalized using a notation based on multi-set rewriting with existential quantification. This presentation describes the multiset rewriting approach to security protocol analysis, algorithmic upper and lower bounds on specific forms of protocol analysis, and some of the ways this model is useful for formalizing sublte properties of specific protocols

12:00-12:30  David Déharbe, Federal U of Rio Grande do Norte, Brazil
Anamaria Martins Moreira, Federal U of Rio Grande do Norte, Brazil
Christophe Ringeissen, LORIA Nancy, France
Improving symbolic model checking by rewriting temporal logic formulae
A factor in the complexity of conventional algorithms for model checking Computation Tree Logic (CTL) is the size of the formulae, and, more precisely, the number of fixpoint operators. This paper addresses the following questions: given a CTL formula f, is there an equivalent formula with fewer fixpoint operators? and how term rewriting techniques may be used to find it? Moreover, for some sublogics of CTL, e.g. the sub-logic NFCTL (no fixpoint computation tree logic), more efficient verification procedures are available. This paper also addresses the problem of testing whether an expression belongs or not to NFCTL, and providing support in the choice of the most efficient amongst different available verification algorithms. In this direction, we propose a rewrite system modulo AC, and discuss its implementation in Elan, showing how this rewriting process can be plugged in a formal verification tool.

Session 7

Chair: Bernhard Gramlich

14:00-14:30  Janis Voigtländer, Dresden U of Techn., Germany
Conditions for efficiency improvement by tree transducer composition
We study the question of efficiency improvement or deterioration for a semantic-preserving program transformation technique based on macro tree transducer composition. By annotating functional programs to reflect the internal property `computation time' explicitly in the computed output, and by manipulating such annotations, we formally prove syntactic conditions under which the composed program is guaranteed to be more efficient than the original program, with respect to call-by-need reduction to normal form. The developed criteria can be checked automatically, and thus are suitable for integration into an optimizing functional compiler.

14:30-15:00  Martin Bravenboer, Utrecht U, The Netherlands
Eelco Visser, Utrecht U, The Netherlands
Application paper: Rewriting strategies for instruction selection
Instruction selection (mapping IR trees to machine instructions) can be expressed by means of rewrite rules. Typically, such sets of rewrite rules are highly ambiguous. Therefore, standard rewriting engines based on fixed, exhaustive strategies are not appropriate for the execution of instruction selection. Code generator generators use special purpose implementations employing dynamic programming. In this paper we show how rewriting strategies for instruction selection can be encoded concisely in Stratego, a language for program transformation based on the paradigm of programmable rewriting strategies. This embedding obviates the need for a language dedicated to code generation, and makes it easy to combine code generation with other optimizations.

15:00-15:30  Olivier Bournez, LORIA Nancy, France
Claude Kirchner, LORIA Nancy, France
Probabilistic rewrite strategies: Applications to ELAN
Recently rule based languages focussed on the use of rewriting as a modeling tool which results in making specifications executable. To extend the modeling capabilities of rule based languages, we explore the possibility of making the rule applications subject to probabilistic choices.
We propose an extension of the Elan strategy language to deal with randomized systems. We argue through several examples that we propose indeed a natural setting to model systems with randomized choices. This leads us to interesting new problems, and we address the generalization of the usual concepts in abstract reduction systems to randomized systems.

Session 8: Tool Demonstrations

Chair: Albert Rubio

16:00-16:20  Jaco van de Pol, CWI Amsterdam, The Netherlands
Tool demonstration: JITty: A rewriter with strategy annotations
We demonstrate JITty, a simple rewrite implementation with strategy annotations, along the lines of the Just-In-Time rewrite strategy. Our tool has the following distinguishing features:
- It provides the flexibility of user defined strategy annotations, which specify the order of normalizing arguments and applying rewrite rules.
- Strategy annotations are checked for correctness, and it is guaranteed that all produced results are normal forms w.r.t. the underlying TRS.
- The tool is `light-weight' with compact but fast code.
- A TRS is interpreted, rather than compiled, so the tool has a short start-up time and is portable to many platforms.

16:20-16:40  Irène Durand, U Bordeaux I, France
Tool demonstration: Autowrite
Autowrite is an experimental tool written in Common Lisp for checking properties of TRSs. It was initially designed to check sequentiality properties of TRSs. For this purpose, it implements the tree automata constructions used in [J96,DM97,DM98,NT99] and many useful operations on terms, TRSs and tree automata (unfortunaletly not all yet integrated into the graphical interface).

16:40-17:00  Benoit Lecland, U Orléans, France
Pierre Réty, U Orléans, France
Tool demonstration: TTSLI: an implementation of tree-tuple synchronized languages
Tree-Tuple Synchronized Languages have first been introduced by means of Tree-Tuple Synchronized Grammars (TTSG), and have been reformulated recently by means of (so-called) Constraint Systems (CS), which allowed to prove more properties.
TTSLI is an implementation of constraint systems, together with the main operations. It is written in Java, and is available on Lecland's web page.

17:00-17:20  Sylvain Lippi, IML Marseille, France
Tool demonstration: in²: A graphical interpreter for interaction nets
in² can be considered as an attractive and didactic tool to approach the interaction net paradigm. But it is also an implementation in C of the core of a real programming language featuring a user-friendly graphical syntax and an efficient garbage collector free execution.

Conference dinner

Joint with FME, LICS
Room: Restaurant Luftkastellet

19:30-21:30  Banquet

21:30-22:30  Martin Davis, U California-Berkeley, USA
Plenary talk: Alan Turing & the advent of the computer