 | |
Sessions
take place in auditorium 3 unless otherwise indicated.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. |
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. |
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. |
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. |
Joint
with FME, LICS
Room:
Restaurant Luftkastellet | 21:30- | 22:30
| Martin Davis, U
California-Berkeley, USA
Plenary
talk: Alan Turing & the advent of the
computer |
| |
![[previous]](../img/prev.gif){kind=small}
![[up]](../img/up.gif){kind=small}
![[next]](../img/next.gif){kind=small}
