Information Flow Analysis via Equational Reasoning
Siva Anantharaman (Université d´Orléans, France)
Gaétan Hains (Université d´Orléans, France)

In this work, process algebra is designed around an ACUID equational theory extended with prefixes symbolizing actions, and by making parallel synchronous composition distributive over non-deterministic choice; such a synchronous composition is commutative and non-associative. Bisimulation between processes is then interpretable as congruence over such an theory. It is shown that information flow analysis is strictly finer when based on bisimulation on these synchronous algebras, than when it is based on trace or weak bisimulation equivalence.

Alpha-prolog, a Fresh Approach to Logic Programming Modulo Alpha-Equivalence
James Cheney (Cornell University, Ithaca, USA)
Christian Urban (University of Cambridge, United Kingdom)

Alpha-prolog is a prototype logic programming language with a built-in notion of binders and unification modulo alpha-equivalence. It is based on a mild extension of first-order Horn formulae: instead of the usual first-order terms and first-order unification, alpha-prolog uses nominal terms and nominal unification introduced in [Urb03]. In this paper, we give three examples that demonstrate the advantages of alpha-prolog and describe our current implementation.

Easy Intruder Deductions
Hubert Comon-Lundh (ENS de Cachan, France)
Ralf Treinen (ENS de Cachan, France)

We investigate extensions of the Dolev-Yao model by some algebraic properties of cryptographic primitives. We provide sufficient conditions under which the intruder deduction problem is decidable (resp. decidable in polynomial time). We apply this result to the equational theory of homomorphism, and show that in this case the intruder deduction problem is linear, provided that the messages are in normal form.

On the Computation of Joins for non Associative Lambek Categorial Grammars
Annie Foret (INRIA, Rennes, France)

This paper deals with an application of unification and rewriting to Lambek categorial grammars used in the field of computational linguistics. Unification plays a crucial role in the acquisition of categorial grammar acquisition, as in [Kan98]; a modified unification has been proposed [For01a] in this context for Lambek categorial grammars, to give an account of their logical part. This modified unification (||=-unification) relies both on deduction (Lambek derivation) and on substitution; it is strongly related to the conjoinability relation [Lam58,Pen93] that is characterized by a free group equivalence and by a quasi-group one in the non-associative version. In view of grammatical inference, we also need to compute joins of the conjoinability relation, when they exists. This paper deals with this issue for the non-associative version of Lambek grammars, and provides an algorithm based on quasi-group rewriting.

Undecidability of Unification over Two Theories of Modular Exponentiation
Deepak Kapur (University of New Mexico, Albuquerque, USA)
Paliath Narendran (SUNY at Albany, USA)
Lida Wang (SUNY at Albany, USA)

Modular multiplication and exponentiation are common operations in modern cryptography. Unification problems with respect to some equational theories that these operations satisfy are investigated. Two different but related equational theories in which the (one-sided) distributivity property of exponentiation over multiplication is assumed are analyzed. The unifiability problem is shown to be undecidable for these two theories.

Applying Unification Techniques to Xml Document Management?
Michael Kohlhase (Carnegie Mellon University, Pittsburgh, USA)

Matching in Flat Theories
Temur Kutsia (Johannes Kepler University Linz, Linz, Austria)

Functional Programming with Sequence Variables: The Sequentica Package
Mircea Marin (Austrian Academy of Sciences, Linz, Austria)

Sequence variables are an advanced feature of modern languages which allows to program in a declarative and easy to understand way. Functional programming with sequence variables relies on the choice of a matcher, which in general is not unique. We propose a number of idioms for programming with sequence variables which enable the user to control the choice of the matcher. To this end we have developed the package Sequentica, which extends the language of Mathematica with our programming constructs. Our extensions enable (1) to control the selection of matcher by annotating sequence variables with priorities and ranges for their lengths, and (2) to compute optimum values characterized by a score function which must be optimized. We illustrate the usefulness of our extensions and describe how they have been implemented.

Satisfiability of Structural Subtype Constraints
Joachim Niehren (Universität des Saarlandes, Saarbrücken, Germany)
Tim Priesnitz (Universität des Saarlandes, Saarbrücken, Germany)

We investigate the satisfiability problem of subtype constraints for the structural case. Our idea is to characterize subtype constraints by formulae in propositional dynamic logic. This approach yields a new result: restricted to crown signatures and models of possibly infinite trees satisfiability of structural subtype constraints is DEXPTIME-complete. This result subsumes and extends the known upper DEXPTIME bound given by Wand and Tiuryn.

A Prefix Notation and Unification Algorithm for Encoding Modal Logics
Adrian Williams (Imperial College, London, United Kingdom)
Jim Cunningham (Imperial College, London, United Kingdom)