ABOUT 
Computer Science Seminars and Short Courses — 2001/02The Computer Science Group holds regular advanced and research level meetings, mainly during the two University teaching semesters. These meetings take the form of Research Seminars, which consist of one hour talks given by invited speakers or members of the Department on current research; Reading Groups which involve a small number of staff and research students studying an advanced book or research paper; and Lecture Courses which are usually delivered by a member of staff and pitched at advanced postgraduate level. Such lecture courses are also taken by staff and research students. Semester 2Seminar programme
Seminar detailsPr Samson Abramsky (Computer Lab, Oxford University) Approximation and Filter Semantics for Combinator Systems Dr Steffen van Bakel (Department of Computing, Imperial College)
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 {BakelFernandezHOA'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.
Noninterference, may testing, and compositionality Dr Steve Schneider (Department of Computer Science, Royal Holloway, University of London)
This talk uses CSP to introduce a characterisation of noninterference 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 noninterference. The CSP characterisation of may noninterference
permits some attractive compositionality proofs. The talk also discusses the
current state of ongoing work to strengthen the characterisation of
noninterference using timed CSP. This approach incorporates the treatment of
refusal testing information within the context of more detailed may testing.
Breaking Symmetry in Matrix Models of Constraint Satisfaction Problems Dr Alan Frisch (The University of York, Department of Computer Science) Many naturallyarising problems can be modelled as a problem of assigning values to a multidimensional matrix of variables so as to satisfy a given set of constraints among the variables. Many of these constraint satisfaction problems have index symmetrya 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 (XP)  dead end or a fresh start for software engineering? Prof Mike Holcombe (The University of Sheffield, Department of Computer Science) 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. Mr Ingmar Meinecke (The University of Dresden, Department of Computer Science)  A complete and minimal programming language for graph transformation Dr Detlef Plump (The University of York, Department of Computer Science)  Dr Michele Zito (The University of Liverpool, Department of Computer Science)  Efficient Communication in AdHoc Radio Networks Dr Leszec Gasieniec (The University of Liverpool, Department of Computer Science) We consider the problem of efficient communication in adhoc radio networks. We will be especially interested in `broadcasting' (onetoall communication) and `gossiping' (alltoall communication). Previous work in the field has been focused on distributed randomized broadcasting algorithms working in unknown adhoc networks, and on deterministic offline broadcasting algorithms assuming full (or at least partial) knowledge of the radio network topology. We start with presentation of adaptive broadcasting algorithms in adhoc radio networks that are simultaneously distributed and deterministic. Then we discuss complexity of an oblivious broadcasting in adhoc 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. Web Information Extraction with LIXTO (Talk and Demo) Prof. Georg Gottlob (TU Vienna) We present a knowledgebased 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 webpages into XML. It can be used to create an "XMLCompanion" for a HTML web page with changing content, containing the continually updated XMLtranslation 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 Modern Concurrency Abstractions for C# Dr Nick Benton (The Microsoft Laboratory, Cambridge) (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. From Total To General Correctness Steve Dunne (The University of Teeside)
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 totalcorrectness
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 generalcorrectness
semantics, which provides a suitable medium for specification and
refinement of such computations. I will highlight the important role
in general correctness of the EgliMilner ordering in providing an
appropriate semantics for recursion, and in particular for loops.
I will relate the generalcorrectness semantics of my abstract
command programs to recent work of Yifeng Chen on reactive systems.
Semester 1Seminar programme
Seminar detailsContention Resolution in MultipleAccess Channels Dr Leslie Ann Goldberg (The University of Warwick, Department of Computer Science) A multipleaccess 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 contentionresolution 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 resending. 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 on infinite objects and descriptive set theory Prof. Victor Selivanov (Novosibirsk Pedagogical University)
Automata working on infinite words and more complicated
objects form a wellestablished 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.
The Classification of Monotonic WellFounded Orderings on Multisets, Strings and Terms Prof Ursula Martin (The University of StAndrews, School of Computer Science) Proving that a computation or process terminates generally requires showing that something is reduced in a wellfounded ordering, and a wide variety of such orderings on common data structures have been devised for the purpose. We investigate the class of montonic wellfounded 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), 921957. Cropper, Nick; Martin, Ursula The classification of polynomial orderings on monadic terms. Appl. Algebra Engrg. Comm. Comput. 12 (2001), 197226. Comparing functional paradigms for exact real arithmetic Dr Alex Simpson (The University of Edinburgh, Division of Informatics) 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. Authenticity by Typing for Security Protocols Dr Andy Gordon (Microsoft Research) 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 spicalculus 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 spicalculus code is welltyped according to a novel type and effect system presented in this paper. Our main theorem guarantees that any welltyped 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 wellknown 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 1113, 2001. Code Streaming: Asynchronous HigherOrder Communication Prof. Masaki Murakami (The University of Okayama)
Static and Dynamic Dictionaries Prof. Torben Hagerup (University of Frankfurt) 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(\logX)$ are acceptable, various classes of balanced trees offer attractive and wellknown 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. Modal logic and inflationary fixed points Dr Anuj Dawar (The University of Cambridge, The Computer Laboratory) The modal mucalculus extends modal (HennessyMilner) logic with a fixedpoint 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 mucalculus. I will also consider decidability and complexity issues that arise for the resulting language. Word problems for 2homogeneous Thue systems and symmetric logspace Dr. Markus Lohrey (University of Stuttgart and Paris 7 (LIAFA)) 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 nhomogeneou Thue systems. A Thue system is called nhomogeneous 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 3homogeneous Thue system with an undecidable word problem, and that every 2homogeneous Thue system has a decidable word problem. Book has sharpened Adjan's decidability result by showing that the word problem for a 2homogeneous Thue system can be solved in linear time. In the talk we will further investigate word problems for 2homogeneous Thue systems. First we will prove that the word problem for every 2homogeneous 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 2homogeneous Thue system is part of the input, is complete for symmetric logarithmic space. Combinatorial algorithms for the maximum generalised network flow problem Dr. Tomasz Radzick (King's College, Department of Computer Science) 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). 

Author: Vincent Schmitt (V.Schmitt@mcs.le.ac.uk), T: 0116 252 3813. 