cms

The talk will be on a recent work with Maribel Fernandez of the ENS. We study the relation between approximation semantics and filter models for Combinator Systems. I will present notions of approximants for terms, intersection type assignment, and using a strong normalization result of \cite {Bakel-Fernandez-HOA'95}, I will show that, for every typeable term, there exists an approximant of that term with the same type. In fact there is a characterization of the normalization behaviour of terms using their assignable types. I will define the approximants semantics and the filter semantics and compare them. The former will be is fully abstract but the latter is not.

This talk uses CSP to introduce a characterisation of non-interference in terms of the deductions that may be made about high level processes by low level tests. May testing yields classic noninference, and has a concise formulation in CSP. It is preserved by a wide range of CSP composition operators, and thus also composes under the operators traditionally studied with non-interference. The CSP characterisation of may non-interference permits some attractive compositionality proofs. The talk also discusses the current state of ongoing work to strengthen the characterisation of non-interference using timed CSP. This approach incorporates the treatment of refusal testing information within the context of more detailed may testing.

Many naturally-arising problems can be modelled as a problem of assigning values to a multi-dimensional matrix of variables so as to satisfy a given set of constraints among the variables. Many of these constraint satisfaction problems have index symmetry--a solution remains a solution if the rows are permuted and the columns are permuted. Unless these index symmetries can removed, or at least greatly reduced, many matrix problems cannot be solved by existing automated methods. This talk will present the results of our ongoing attempt to break symmetries in matrix models. The talk assumes no background in constraint satisfaction, so it should be accessible to all mathematicians and computer scientists.

Extreme programming is another new fad - or is it. It presents us with a number of paradoxes - it is revlutionary yet it is nothing really new. Many comment "I've been doing that for years," or " that's how we used to work before Software Engineering was invented!".

We will present the main ideas of XP and discuss some of its possible strengths and weakness. Some new ideas are discussed that seem to help to improve the process.

Empirical evaluations of the approach are being carried out at Sheffield and some interim results will be reported from these experiments.

-

-

-

We consider the problem of efficient communication in ad-hoc radio networks. We will be especially interested in `broadcasting' (one-to-all communication) and `gossiping' (all-to-all communication).

Previous work in the field has been focused on distributed randomized broadcasting algorithms working in unknown ad-hoc networks, and on deterministic off-line broadcasting algorithms assuming full (or at least partial) knowledge of the radio network topology.

We start with presentation of adaptive broadcasting algorithms in ad-hoc radio networks that are simultaneously distributed and deterministic. Then we discuss complexity of an oblivious broadcasting in ad-hoc radio networks. Finally we show how to perform efficient radio gossiping both in deterministic as well as in random setting.

We conclude the presentation with a list of open problems in the field.

We present a knowledge-based method for the definition of HTML/XML wrappers and a fully visual interface for the generation of wrappers based on that method. We also demonstrate the LIXTO tool, which implements the proposed techniques. LIXTO is portable (implemented with Java), offers a capacious interactive visual interface, allows for expressive and flexible data extraction and uses intuitive hierarchical extraction, as well as string extraction techniques. LIXTO translates relevant parts of web-pages into XML. It can be used to create an "XML-Companion" for a HTML web page with changing content, containing the continually updated XML-translation of the relevant information. Lixto is of high expressive power as it captures Monadic Second Order Logic over unranked trees (i.e., Web documents).

Joint work with Robert Baumgartner, Christoph Koch, and Sergio Flesca. Papers on LIXTO can be found at lixto.com or at http://www.dbai.tuwien.ac.at/proj/lixto/download.html

(joint work with Luca Cardelli and Cedric Fournet)

Polyphonic C# is an extension of the C# language with new asynchronous concurrency constructs, based on the Join Calculus. I'll describe the design and implementation of the language and give examples of its use in addressing a range of concurrent programming problems.

In the formal methods literature specifications have hitherto invariably been expressed, and their refinements conducted, exclusively in the context of total correctness. It is then perhaps surprising that orthodox total-correctness semantics is inadequate for the specification of such a familiar and important class of computations as partial decision procedures. Such computations can only be meaningfully described, at whatever level of abstraction, by general correctness. I will present a simple abstract command language, derived from Abrial's Generalised Substitution Language but endowed with a general-correctness semantics, which provides a suitable medium for specification and refinement of such computations. I will highlight the important role in general correctness of the Egli-Milner ordering in providing an appropriate semantics for recursion, and in particular for loops. I will relate the general-correctness semantics of my abstract command programs to recent work of Yifeng Chen on reactive systems.

A multiple-access channel is an uncontrolled communication channel such as an Ethernet. Users communicate by sending messages to the channel. If two or more users simultaneously send messages, then the messages interfere with each other (collide), and the messages are not transmitted successfully. The users use a contention-resolution protocol to resolve collisions. Thus, after a collision, each user involved in the collision waits a random amount of time (which is determined by the protocol) before re-sending.

Informally, a protocol is said to be "stable" if the messages get delivered as they arrive, without a big backlog building up. (I'll be more precise about this in the talk.)

It is still not fully understood which protocols are stable and which are not. I will survey the known results and the methods which are used in the area, and will discuss open problems.

Automata working on infinite words and more complicated objects form a well-established topic of theoretical informatics related to such practically important problems as specification, verification and synthesis of hardware and software systems. We will discuss some recent applications of modern descriptive set theory (in particular, Wadge hierarchy of Borel sets) to this topic. These applications simplify some older technically difficult results of Klaus Wagner and yield many new interesting results and new research directions in this field.

Proving that a computation or process terminates generally requires showing that something is reduced in a well-founded ordering, and a wide variety of such orderings on common data structures have been devised for the purpose.

We investigate the class of montonic well-founded orderings on multisets, strings and terms and show that despite the apparent diversity they can be studied in a unifying framework that provides logical and numeric invariants for the different orderings.

An initial understanding is provided by the order type, which has intrigung connections with recursion theory. We outline a finer classification, showing that in each case the relevant orders are essentially extensions of an order by weight. This allows us to associate numerical invariants to orders, to show that several previously studied orderings were equivalent and to reduce some termination proofs to constraint solving.

We also survey possible applications and extensions in fields as diverse as computational biology and abstract algebra.

Martin, Ursula; Shand, Duncan Invariants, patterns and weights for ordering terms. J. Symbolic Comput. 29 (2000), 921--957.

Cropper, Nick; Martin, Ursula The classification of polynomial orderings on monadic terms. Appl. Algebra Engrg. Comm. Comput. 12 (2001), 197--226.

joint work with Andrej Bauer and Martin Escardo

There are two standard approaches to exact real number computation within functional programming. Under one approach, real numbers are represented using an ordinary data type (for example, integer streams), and operations on them are implemented as functions on this type. In the second approach, the representation is hidden by encapsulating real numbers within an abstract data type. In the talk, I will first give an overview of the two approaches, and then discuss preliminary results from a general investigation relating the two.

Based on joint work with Alan Jeffrey, DePaul University

We propose a new method to check authenticity properties of cryptographic protocols. First, code up the protocol in the spi-calculus of Abadi and Gordon. Second, specify authenticity properties by annotating the code with correspondence assertions in the style of Woo and Lam. Third, figure out types for the keys, nonces, and messages of the protocol. Fourth, check the spi-calculus code is well-typed according to a novel type and effect system presented in this paper. Our main theorem guarantees that any well-typed protocol is robustly safe, that is, its correspondence assertions are true in the presence of any opponent expressible in spi. It is feasible to apply this method by hand to several well-known cryptographic protocols. It requires little human effort per protocol, puts no bound on the size of the opponent, and requires no state space enumeration. Moreover, the types for protocol data provide some intuitive explanation of how the protocol works. Our method has led us to the independent rediscovery of flaws in existing protocols and to the design of improved protocols.

The talk describes our method and gives some simple examples. A paper describing the method appears in the proceedings of the 14th IEEE Computer Security Foundations Workshop, June 11--13, 2001.

A static dictionary for a set $X$ of keys with associated satellite information is a data structure that can answer queries of the form ``Is $x\in X$ and, if so, which is the associated satellite information?'' A dynamic dictionary additionally supports changes to the key set $X$ through insertions and deletions. If query times of $\Theta(\log|X|)$ are acceptable, various classes of balanced trees offer attractive and well-known realizations of dynamic dictionaries. When sublogarithmic query times are desired, however, dictionaries are frequently realized with methods based on hashing. The talk provides an overview, from a theoretical point of view, of static and dynamic dictionaries that were developed in recent years to satisfy many different requirements. The focus will be on central ideas and general principles, not on technical detail.

The modal mu-calculus extends modal (Hennessy-Milner) logic with a fixed-point operator, useful for specifying recursive properties. I will consider a variant of the calculus involving an iterative (or inflationary) operator in place of the least fixed point. While in many logical contexts, least fixed points and inflationay fixed points are interchangeable, I will show how in this case the inflationary operator leads to greater expressive power than the mu-calculus. I will also consider decidability and complexity issues that arise for the resulting language.

Since the work of Markov and Post it is known that there exist Thue systems with undecidable word problems. In order to locate the borderline between decidability and undecidability for word problems, Adjan has introduced the notion of a n-homogeneou Thue systems. A Thue system is called n-homogeneous for some $n \in \mathbb{N}$ if every rule is of the form $s \to \epsilon$, where $\epsilon$ is the empty word and $s$ is a word of length $n$. Adjan has shown that there exists a fixed 3-homogeneous Thue system with an undecidable word problem, and that every 2-homogeneous Thue system has a decidable word problem. Book has sharpened Adjan's decidability result by showing that the word problem for a 2-homogeneous Thue system can be solved in linear time.

In the talk we will further investigate word problems for 2-homogeneous Thue systems. First we will prove that the word problem for every 2-homogeneous Thue system can be even solved in logarithmic space. This generalizes a result of Lipton and Zalcstein for free groups. Furthermore we show that a uniform version of the word problem, where a 2-homogeneous Thue system is part of the input, is complete for symmetric logarithmic space.

We consider the following generalised network flow model: If f(v,u) units of flow enter edge (v,u) at node v and the gain/loss factor of this edge is g(v,u), then g(v,u)f(v,u) units of flow arrive at node u. The objective function we consider is to maximize the net flow into a specified sink node. This optimisation problem arises in manufacturing, transportation and financial analysis. In this talk we review combinatorial algorithms for the maximum generalised flow problem, in particular the algorithms which have asymptotically fastest published running time of O(m^3 log B). We also sketch our recent idea of demonstrating that this asymptotic running time can be reduced further to O(m^2 n log B).