ABOUT 
Computer Science Seminars and Short Courses — 2004/05You main need this to find your way...
Semester 2Seminar programme
Seminar detailsNew approximation algorithms for the set cover problem Dr Asaf Levin (The Hebrew University of Jerusalem) In the weighted setcover problem we are given a set of elements $E=\{ e_1,e_2, \ldots ,e_n \}$ and a collection $\cal F$ of subsets of $E$, where each $S \in$$\cal F$ has a positive cost $c_{S}$. The problem is to compute a subcollection $SOL$ such that $\bigcup_{S\in SOL}S_j=E$ and its cost $\sum_{S\in SOL}c_S$ is minimized. When $S\le k\ \forall S\in\cal F$ we obtain the weighted $k$set cover problem. The special case of the weighted $k$ set cover where each set has a unit cost, is called the unweighted $k$set cover problem. It is well known that the greedy algorithm is an $H_k$approximation algorithm for the weighted (and unweighted) $k$set cover, where $H_k=\sum_{i=1}^k {1 \over i}$ is the $k$th harmonic number, and that this bound is exact for the greedy algorithm for all constant values of $k$. The previous best improvement of the greedy algorithm for the unweighted $k$set cover problem is an $\left( H_k{1\over 2}\right)$approximation algorithm. In the first part of the talk I will present a new $\left( H_k{196\over 390}\right)$approximation algorithm for $k \geq 4$ that improves the previous best approximation ratio for all values of $k\geq 4$. This algorithm is based on combining local search during various stages of the greedy algorithm. In the second part of the talk I will present the first improvement on the approximation ratio of the greedy algorithm for the weighted $k$set cover problem for all constant values of $k$. This result shows that the greedy algorithm is not the best possible for approximating the weighted set cover problem. Our method is a modification of the greedy algorithm that allows the algorithm to regret. A part of this talk is based on a joint work with Rafi Hassin. Online Bin Packing with Cardinality Constraints Dr Leah Epstein (The University of Haifa)
We consider a one dimensional storage system where each container
can store a bounded amount of capacity as well as a bounded number
of items k>1. This defines the (standard) bin packing problem with
cardinality constraints which is an important version of bin
packing, introduced by Krause, Shen and Schwetman already in 1975.
Following previous work on the unbounded space online problem, we
establish the exact best competitive ratio for bounded space
online algorithms for every value of k. This competitive ratio is
a strictly increasing function of k which tends to approximately
2.69103 for large k. Lee and Lee showed in 1985 that the best
possible competitive ratio for online bounded space algorithms
for the classical bin packing problem is the sum of a series, and
tends to one less than the above value as the allowed space
(number of open bins) tends to infinity.
We further design optimal online bounded space algorithms for
variable sized bin packing, where each allowed bin size may have
a distinct cardinality constraint, and for the resource
augmentation model. All algorithms achieve the exact best
possible competitive ratio possible for the given problem, and
use constant numbers of open bins.
Finally, we introduce unbounded space online algorithms with
smaller competitive ratios than the previously known best
algorithms for small values of k, for the standard cardinality
constrained problem. These are the first algorithms with
competitive ratio below 2 for k=4,5,6.
Dr HansArno Jacobsen (The University of Toronto) Over the past decade, middleware platforms such as CORBA, J2EE, and Web Services have become increasingly popular, addressing software engineering problems for distributed application development in the most diverse application domains and under greatly varying requirements. For many of these platforms, these proliferations have led to complicated architectures, complex abstractions, and bloated implementations. We think, this is mainly due to the interaction of too many (crosscutting) concerns, imposed from a wide range of requirements, and the lack of being able to adequately modularize these concerns. For example, it is not possible to easily customize a given middleware implementation or flexibly adapt it to address ever changing domain requirements. In this talk we will present results drawn from our ongoing Aspect Oriented Middleware research project. We will first present examples illustrating the phenomenon of logic tangling and implementation convolution, which we believe to be central for the above outlined problems. This phenomenon is not due to bad design but rather due to the limitations of conventional architectural decomposition methodologies. We will show how aspect oriented programming (AoP) techniques can remedy this problem. We will present results on quantifying logic tangling in several existing middleware implementations through aspect mining. We will briefly review our mining methodology and, timepermitting, describe our Eclipsebased, Prism tool chain, which we have developed to aid in the discovery of aspects in large code bases. Our aspect mining results clearly indicate the inherent presence of aspects in (legacy) platform implementations. Moreover, our extensive aspect oriented refactoring efforts strongly suggest that AoP can improve the customization, configurability, modularity, and computational efficiency of an aspect oriented middleware implementation. This research is joint work with Charles Zhang Syntactic Characterisations of PolynomialTime Optimisation Classes Dr Prabhu Manyem (School of Information Technology and Mathematical Sciences  University of Ballarat)
In Descriptive Complexity, there is a vast amount of literature on
decision problems, and their classes such as P, NP, L and NL.
However, research on optimisation problems has been limited.
Optimisation problems corresponding to the NP class have been
characterised in terms of logic expressions by Kolaitis and Thakur,
Panconesi and Ranjan, and by Zimand. Here, we attempt to characterise
the optimisation versions of subclasses of P via expressions in
second order logic, many of them using universal Horn formulae with
successor relations.
Proof Preserving Transformations Dr Piotr Kosiuczenko (The University of Leicester)
Redesign of a structure requires transformation of the corresponding specification. In this talk we will discuss the way proof are transformed via, what we call, interpretation functions. We provide a sufficient condition for such functions to preserve proofs in equational logic, as well as proofs in other logical systems such as propositional logic with modus ponens, proofs using resolution rule and induction. This results allow us to identify a class of specification preserving system redesigns.
A Formal Approach to Service Specification and Matching based on Graph Transformation Dr Reiko Heckel (The University of Leicester) When Web services are composed by linking service providers and requestors, the requestor\u2019s requirements for a \u201duseful\u201d service have to be matched against the service description offered by the provider. Among other things, service specifications (requirements or descriptions) may contain operation contracts specifying preconditions and effects of (required or provided) operations. In this presentation we provide a semiformal, UMLbased notation for contracts and contract matching, as well as a formalization of these notions in terms of graph transformation. We establish the desired semantic relation between requestor and provider specifications and prove the soundness of our syntactic notion of matching w.r.t. this relation. Reversing CCS with Onetime Communication Keys Dr Irek Ulidowski (The University of Leicester)
Reversibility of Milner's CCS has been studied by Danos and Krivine in their language RCCS, which uses separate memories and labels transitions with information about threads. We introduce a different approach, where processes maintain their structure as they evolve. We keep track of communications by binding together the two partner processes with ``communication keys'', which are generated freshly for each new communication. Just as with RCCS, we can use the calculus to model reversible biological reactions.
FireWorks: A Formal Transformational Approach to Features (joint work with Mark Ryan) Dr PierreYves Schobbens (L'Universite' de Namur )
The FireWorks approach to features is based on development by refinements.
But we assume that the base product is refined through a domain defined levels.
Additions on this base product are defined as transformations at each level.
Transformations can be initially as simple as the replay of the editions operations used to obtain
the enhanced product, but will then be improved to work on a larger class of base products.
We are specially interested by applying the transformation the result of a previous transformation (feature), and we can define it by cases for this purposes, but it is better to obtain a single, uniform
transformation able to deal also with intially unforeseen features.
This gives us the basis to define a first type of feature interference: when the levels obtained by composing the features are no longer refinements.
Features that preserve refinement can thus be proved to never yield interference of this type.
Up to now, we mainly used substitutions as the transformations representing features, but more is possible. Specially, for graphical formalisms, some graph transformations could be adequate.
Dr FerJan de Vries (The University of Leicester) The application of rewriting theory to functional languages leads naturally to the consideration of infinite rewriting sequences and their limits. Our theory of transfinite rewriting puts this intuitive concept on a sound footing through the concept of a strongly convergent rewriting sequence, of which the crucial property is that not only does the sequence of terms tend to a limit, but the sequence of redex positions tends to infinite depth. This notion allows us to demonstrate some classical results for orthogonal systems. However, it transpires that the most important of these, confluence, fails in certain cases. These cases can be precisely characterised, and confluence can be reestablished modulo the equality of the set of terms which obstruct precise confluence. The offending terms are of a form that can reasonably be viewed as representing infinite computations that produce no result, and in this sense are undefined. Further consideration of this set of terms reveals that any set which satisfies certain natural axioms can serve as the class of undefined terms. All this leads to the following construction on a finite orthogonal system R: (0) identify a set of undefined terms. (1) add a new bottom element to the syntax (2) consider the set of finite and infinite terms (3) add a new rule that rewrites undefined terms to bottom This infinite extension of R is confluent and normalising and yields immediately a syntactic model of the original orthogonal system. For the lambda calculus this has yielded a new uniform characterisation of several known models (eg the Boehm model), and a construction of many more. The latter is current work in progress by Paula Severi and me. Dr Marc Aiguier (L'Universite'd'Evry  France)
When rewriting is used to generate convergent and complete rewrite systems
in order to answer the validity problem for some theories, all the
rewriting theories rely on a same set of notions, properties and
methods. Rewriting techniques have mainly been used to answer the validity problem of
equational theories, that is to compute congruences. However, recently, they have
been extended in order to be applied to other algebraic structures
such as preorders and orders. In this talk, we investigate an abstract form of rewriting,
by following the paradigm ``logicalsystem independent''. Hence, we provide a few simple
conditions (or axioms) under which rewriting (and then the set of
classical properties and methods) can be modeled, understood, studied,
proven and generalized. This enables us to extend rewriting techniques
to other algebraic structures than congruences and preorders such as
congruences closed under monotonicity and modusponens. This allows us
to introduce convergent rewrite systems, and to describe both deduction procedures for
their corresponding theory and a KnuthBendix style
completion procedure.
Operational domain theory and topology of a sequential programming language. Dr Weng Kin Ho (The University of Birmingham) A number of authors have exported domaintheoretic techniques from denotational semantics to the operational study of contextual equivalence and preorder. We further develop this, and, morover, we additionally export topological techniques. In particular, we work with an operational notion of compact set and show that the total programs with values on certain types are uniformly continuous on compact sets of total elements. We apply this and other conclusions to prove the correctness of nontrivial programs that manipulate infinite data. What is interesting is that the development applies to sequential programming languages. Paper: M.H. Escardo and W.K. Ho. Operational domain theory and topology of a sequential programming language. LICS 2005. See http://www.cs.bham.ac.uk/~mhe/papers/index.html Structured CSP  A Process Algebra as Institution Dr Markus Roggenbach (The University of Swansea) In this talk we extend the process algebra CSP by a 'module concept' that allows us to build complex specifications out of simpler ones. Here we reuse typical structuring mechanisms from algebraic specification as they are realised, e.g., in the algebraic specification language CASL. We demonstrate through various examples that these structuring mechanism (e.g. extension, union, renaming, parametrisation) are suitable for CSP. On the theoretical side our approach requires us to formulate the process algebra CSP as an institution. We show that the CSP trace model fits into this setting. Besides the practical outcome in the form of a module concept for CSP, this formulation can also be seen as a natural framework for stating process algebraic laws. Furthermore, formulating a process algebra as an institution links two hitherto unrelated specification formalisms. Dr Alexander Hall (ETH Zurich)
Kenyon et al. (STOC 04) compute the distortion between onedimensional
finite point sets when the distortion is small; Papadimitriou and Safra
(SODA 05) show that the problem is NPhard to approximate within a
factor of 3, albeit in 3 dimensions. We solve an open problem in these
two papers by demonstrating that, when the distortion is large, it is
hard to approximate within large factors, even for 1dimensional point
sets. We also introduce additive distortion, and show that it can be
easily approximated within a factor of two.
This is joint work with Christos Papadimitriou.
Foundations of Modular Structural Operational Semantics Pf P.D. Mosses (The University of Swansea) Modular SOS (MSOS) is a variant of conventional Structural Operational Semantics (SOS). Using MSOS, the transition rules for each construct of a programming language can be given incrementally, and they do not need reformulation when further constructs are added to the described language. MSOS thus provides an exceptionally high degree of modularity in semantic descriptions, removing a shortcoming of the original SOS framework. The crucial feature of MSOS is that labels on transitions are now morphisms of a category, and exploited to ensure the appropriate flow of information (such as environments and stores) during computations. The talk explains the foundations of MSOS, and illustrates how MSOS descriptions are written in practice. It also discusses standard notions of semantic equivalence for MSOS, and indicates how MSOS descriptions can be translated to Prolog. Familiarity with the basic ideas of conventional SOS and labelled transition systems is assumed. The canonical relation lifting and coalgebraic modal logic Dr Bartek Klin (The University of Sussex)
In the coalgebraic approach to statebased processes, relation
lifting is used to model bisimulation abstractly. On the other hand,
predicate lifting is used in coalgebraic modal logics. I will consider
both liftings in a fibrational setting, show how they are related, and
describe how the least relation liftings give rise to modal logics
expressive for a wide class of functors. In the resulting logics,
modalities of multiple arity can appear.
Energy efficient broadcast trees in the Euclidean plane Christoph Ambühl (Dalle Molle Institute for Artificial Intelligence Lugano) Computing energy efficient broadcast trees is one of the most prominent operations in wireless networks. For stations embedded in the Euclidean plane, the best analytic result known to date is a 7.6approximation algorithm based on computing an Euclidean minimum spanning tree. We improve the analysis of this algorithm and show that its approximation ratio is 6, which matches a previously known lower bound for this algorithm. The main ingredient of the proof is the following lemma: Let S be any point set which  is a subset of the unit disk around the origin and  includes the origin. Let T be the Euclidean minimum spanning tree of S. Then the sum of the squared edge lengths of T is bounded by 6. OMML: A Behavioural Model Interchange Format Dr Andrea Zisman (City University London)
Large distributed systems are normally developed by combining various nodes that are produced by different stakeholders, using different technologies, languages, and formalisms. The number and diversity of existing languages for describing behavioural specifications (models) of systems do not enable the integration, sharing, or reuse of models between tools. Incompatible node models cannot be used to help validate overall combined system behaviour. In this talk we present an XMLbased model interchange format named OpenModel Modeling Language (OMML). OMML is part of a large project of research called OpenModel to support design, analysis, and validation of multistakeholder distributed systems. OMML is a function rich procedural language that expresses functionality in terms of function/object theories and represents behavioural models in a toolindependent way. OMML is composed of 5 different document types describing executable specification models of the services running at the nodes, information about connections between the various nodes, information about the (abstract) state of the services, and domain specific information to allow standardisation of the terminology used by model developers. We present how OMML can be used to support interchange of models in email, instant messaging, and web services applications. We discuss prototype tools that we have developed to support translation between models expressed in PEBF, OMML, and SCR and evaluate our approach by validating applications composed of models expressed in different languages in the GSTView validation tool.
Inductiverecursive definitions and generic programming Dr Anton Setzer (The University of Wales  Swansea) (joint work with P. Dybjer, Gothenburg, Sweden) We give a brief introduction into dependent type theory and its role in generic/generative programming. We then investigate the basic constructs for introducing types in dependent type theory and generalize it to the notion of inductiverecursive definitions. We then introduce a data type of inductiverecursive definitions and discuss how this data type can be used for defining generic functions, which can not only take elements of data types, but as well codes for data types, and generate from it both codes for data types and elements of those types. Automatic Presentations for Finitely Generated Groups Graham Oliver (The University of Leicester) Structures presentable by finite automata are of growing interest, particularly as the closure properties of automata give a generic algorithm for deciding first order properties. One catalyst for this idea was the theory of automatic groups, which has been useful in developing implementable algorithms for grouptheoretic problems. However, the theories are not equivalent. The classification presented here, of those finitely generated groups which have automatic presentations, allows a direct comparison; it also adds to the limited number of classification theorems already established. Nominal Reasoning Techniques in Isabelle/HOL Dr C. Urban (The University of München) I will describe how standard (informal) proofs about the lambdacalculus can be formalised with ease in Isabelle/HOL using a variant of Pitts' nominal logic work. First, I shall present an inductive definition for alphaequated lambdaterms and then a strong induction principle that looks very much like the Barendregt variable convention. The technical novelty of my work is that it is compatible with the axiomofchoice and therefore can be based on standard settheory. Predicate transformers, predicatively Dr Peter G. Handcock In the refinement calculus (Back and von Wright, Morgan, et al) predicate transformers model both specifications and programs. It involves a nice category in which the objects are monotone predicate transformers over a statespace, and the morphisms are socalled downward simulations. The natural logical habitat of this category is impredicative higherorder classical logic. By putting together some notions in the literature of constructive mathematics one can reconstruct this category in a fully constructive setting such as MartinLof's type theory. This gives a "working" model of commandresponse interfaces and components. Joint work with Pierre Hyvernat (Chalmers/Marseilles) and Anton Setzer (Swansea). Categorical Quantum Mechanics: a highlevel approach for quantum computation and information Dr Bob Coeke (Oxford University Computing Laboratory) The current methods available for developing quantum algorithms and protocols are deficient on two main levels. Firstly, they are too lowlevel. One finds a plethora of ad hoc calculations with `bras' and `kets', normalizing constants, matrices etc. The arguments for the benefits of a highlevel, conceptual approach to designing, programming and reasoning about quantum computational systems are just as compelling as for classical computation. Moreover, there is the whole issue of integrating quantum and classical features, which would surely be mandatory in any practicable system. At a more fundamental level, the standard mathematical framework for quantum mechanics (due to [von Neumann 1932]) is actually insufficiently comprehensive for informatic purposes: in particular, the flow of information from quantum to classical arising from measurements, and the dependence of subsequent stages of the computation on this information, is not adequately covered by the standard formalism. As quantum protocols and computations grow more elaborate and complex, this point is likely to prove of increasing importance. In [Abramsky and Coecke 2004] we addressed these problems, the key ingredient being a purely *categorical axiomatization of quantum mechanics* The concepts of abstract quantum mechanics are formulated in any *strongly compact closed category with biproducts* (of which the category FdHilb of finite dimensional Hilbert spaces and linear maps is an example). Preparations, measurements, and classical data exchange are all morphisms in the category, and their types fully reflect their kinds. Correctness properties of standard quantum protocols such as quantum teleportation can be proved at this abstract level. In particular, due to the compositional nature of quantum entanglement in this abstract formalism, proofs actually become much simpler, and so does the discovery of new protocols. Although this setting seems purely qualitative, in fact even the Born rule, which specifies how probabilities are calculated, can be derived in it. J. von Neumann. Mathematische Grundlagen der Quantenmechanik. SpringerVerlag (1932). English translation in Mathematical Foundations of Quantum Mechanics. Princeton University Press (1955). S. Abramsky and B. Coecke. A categorical semantics of quantum protocols. In the proceedings of LiCS'04 (2004). An extended version is available at arXiv:quantph/0402130 Algebra for Information Update in MultiAgent systems Dr Mehrnoosh Sadrzadeh
(Oxford University Computing Laboratory) Joint work with A. Baltag and B. Coecke We model information flow in multiagent systems where communication between agents changes the information state of each agent. I shall first present an alternative and more general nonboolean algebraic semantics for the usual Kripke structures used in dynamic epistemic logic (e.g. BaltagMoss). This algebraic setting consists of an epistemic system (M,Q,{f_A}_{A \in {\cal A}}), which is a quantalemodule pair (M,Q) endowed with a family of "appearance maps" for each agent f_A = (f_A^M: M >M, f_A^Q:Q >Q). These maps satisfy some natural conditions. The right Galois adjoint to the appearance map gives rise to the "box" modality of epistemic logic (expressing knowledge or belief of some agent). The algebra can be used to encode and solve, in an elegant manner, standard dynamic epistemic puzzles such as "cheating muddy children" . I will also present a complete sequent calculus with regard to our algebra and apply it to an example of a security protocol. Finally, I shall briefly show how moving to a supenriched categorical setting allows us to relativize information updates to agents and thus deal with classical problems such as logical omniscience. On minimizing the number of ADMs in WDM/SONET rings Dr Alexey Fishkin (MaxPlanck Institute Informatik, Saarbruecken) SONET (Synchronous Optical NETworks) adddrop multiplexers (ADMs) are the dominant cost factor in the WDM (Wavelength Division Multiplexing)/SONET rings. The number of SONET ADMs required by a set of traffic streams is determined by the lightpath routing and wavelength assignment of the traffic streams. We address the WDM/SONET ring network design problem where each traffic stream has a predetermined routing given by a lightpath, and a careful wavelength assignment for the ligthpaths is used to minimize the number of SONET ADMs. This can be modeled as the problem of partitioning a set of circular arcs over a ring into segments of nonintersecting arcs where the objective is to minimize the number of noncircle segments. We present and analyse two randomized approximation algorithms. Semester 1Seminar programme
Seminar detailsData Types for Differentiable Functions Dr Dirk Pattinson (Ludwig Maximilien University (München), on leave at Imperial College) We introduce a domaintheoretic computational model for multivariable differential calculus, which gives rise to datatypes for differentiable functions. The model, a continuous Scott domain for differentiable functions of n variables, is built as a subdomain of the product of n+1 copies of the function space on the domain of intervals by tupling together consistent information about locally Lipschitz (piecewise differentiable) functions and their differential properties (partial derivatives). We show, in two stages, that consistency is decidable on basis elements and discuss two applications of our model: The effective calculation of inverse and implicit functions and improved methods for solving initial value problems. How to untie knots in stores: HoareLogic for HigherOrder Store Bernhard Reus (The University of Sussex) We present a Hoare logic for a simple imperative whilelanguage with stored commands, ie. stored parameterless procedures. Stores that may contain procedures are often called higherorder. Soundness of our logic is established by using denotational rather than operational semantics. The former seems more suitable as it elegantly accounts for an inherent difficulty of higherorder store, namely that assertions necessarily describe recursive predicates on a recursively defined domain. Our findings should be relevant to logics for objectoriented languages where methods can be loaded or created at runtime. Towards a Calculus for the Development of Security Protocols Dr Gavin Lowe (Oxford) During the last 10 years, we've become pretty good at analysing security protocols. However, we still lack a solid framework for designing correct protocols: the best technique we have is to use our experience and judgement to come up with a protocol that we think is correct, and then to verify it. This is the question this research addresses. I will outline a calculus for developing correct security protocols. Protocol descriptions are annotated with assertions that state properties that will be true when the protocol execution reaches that point; I will give some proof rules that allow the assertions to be verified. A novel feature of the calculus is that the initial development of a protocol uses abstract messages that describe the intention of a message, rather than the concrete implementation; I will outline some rules that allow these abstract messages to be suitably implemented. I will sketch the semantic model that is used to formalise the calculus, and illustrate it with some examples. Empirical studies of Software evolution  The last 20 years Dr J.F.Ramil (Computing Dept., The Open University, UK) Informally speaking, software evolution is what happens after the first operational release. More formally, software evolution is the process of continual software change. The term is mainly used to refer to enhancements, adaptations and fixes that occur after the first version of a software system is released to its users. According to different surveys, the largest portion of effort is subsumed by software evolution, not by initial development. In a 1984 IEEE TSE paper, Prof Barry Boehm indicated the area of modelling of the software lifecycle evolution as one of seven outstanding issues in software engineering economics. Despite the advances in understanding during the last 20 years, this is still an active area of research with many unanswered questions. For example, in an world driven by shortterm gains, it is still not clear how one can decide how much refactoring and restructuring effort should be applied in order to maximize the value that a software system provides to its stakeholders. This talk will summarise our findings in the study of Open Source evolution and their implications for implementing and managing software evolution. The talk will also argue for quantitative models and views that reflect different levels of abstraction and aggregation (macroevolution and microevolution) in order to derive a richer, more meaningful and useful picture of the long term evolution of a software system. Juan F. Ramil is a lecturer at the Computing Dept., The Open University. He joined the OU in October 2001 after five years or so as a researcher at Imperial College London. Andrea Capiluppi is a visiting researcher at the Computing Dept., The Open University, Milton Keynes, UK. He is planning to submit his PhD thesis at the Dipartimento of Automatica e Informatica, Politecnico of Torino, Italy, early in the next year. Recent advances in Dependent Type Theory Dr Nicola Gambino (The University of Cambridge, UK) Dependent type theories have been considered both as foundational frameworks for constructive mathematics, and as programming languages for the simultaneous development of programs and specifications. In my talk, I will discuss some recent work on dependent type theories, developed in collaboration with Peter Aczel and Martin Hyland. Much of this research focuses on relating dependent type theories, constructive set theories, and categorical structures. The connections between these three settings leads to some nice prooftheoretic applications. Modular Construction of Modal Logics Dr Corina Cirstea (The University of Southampton) (joint work with Dirk Pattinson) The coalgebraic approach to modelling statebased systems allows various system combinations to be modelled at the level of coalgebraic signatures using operations such as functor composition, product or coproduct. We show that this modularity at the level of signatures can be lifted to a logical level, thereby allowing the derivation of logics for coalgebras of functor combinations from logics for coalgebras of the functors being combined. Furthermore, we show that relevant properties of the logics, including expressiveness, soundness and completeness, are preserved by these operations for combining logics. These results are used to derive expressive, sound and complete logics for a large class of probabilistic system types. Intersection Types and Lambda Models Pr Mariangiola Dezani (Universita di Torino  Departimento di Informatica) Intersection types can be viewed also as a restriction of the domain theory in logical form, to the special case of modelling pure lambda calculus by means of omegaalgebraic complete lattices. Intersection types have been used as a powerful tool both for the analysis and the synthesis of lambda models. On the one hand, intersection type disciplines provide finitary inductive definitions of interpretation of lambda terms in models. On the other hand, they are suggestive for the shape the domain model has to have in order to exhibit certain properties. Problem and Solution Structures Pr Michael Jackson (The Open University) Problem decomposition in softwareintensive systems is discussed, and some general principles and ideas are presented. For a problem decomposed into subproblems the task of composing the results demands attention, in both the problem and solution domains. It is recommended to postpone considering composition until the subproblems to be composed have been analysed and understood. Vincenti's distinction between radical and normal engineering is explained. Software developers should practise normal engineering wherever possible. System Codevelopment through Requirements Specification Professor Pericles Loucopoulos (UMIST) Some of the most challenging system development projects involve multiple stakeholders from different participating organisations, subcontractors, divisions etc who may have a diversity of expertise, come from different organisational cultures and often have competing goals. The relatively recent emphasis on processcentred approaches has highlighted the need for appropriate mechanisms for the elicitation, representation and validation of requirements that focus on the codevelopment activity whose aim is to ensure alignment between business processes and support technical systems. A key challenge in the development of systems is the engagement of domain experts in their articulation, agreement, and validation of requirements. This challenge is particularly pronounced at the socalled early requirements phase when multiple stakeholders from different divisions and often different organisations need to reach agreement about the intended systems. Decisions taken at this stage have a profound effect on the technical and economic feasibility of the project. It is no longer appropriate for information systems professionals to focus only on functional and nonfunctional aspects of the intended system and somehow assume that organisational context and needs are outside their remit. Traditional requirements engineering (RE) techniques that have emerged over the years in the field of information systems engineering are also being applied to business process modelling. In both cases modelling is advocated as a way of facilitating analystclient communication. In both cases the focus of the modelling paradigm is on requirements for support systems rather than on codevelopment issues. In neither case does a modelling paradigm is specifically deployed to facilitate communication between stakeholders and since early requirements elicitation is founded on the need for stakeholders to cooperatively reach agreement on the interactive and interdependent nature of all requirements in their totality, neither class fully tackles the problems of early requirements. This talk will critically examine contemporary approaches to early requirements modelling, discuss the main issues that should be addressed by modelling and propose an approach that arguably provides a solid and usable framework for addressing the key problem of early requirements namely, engaging stakeholders in defining, exploring and validating early requirements. Examples from large industrial applications, involving business process reengineering and enterprise integration will be given to highlight the key issues raised in this talk. Modelling a biochemical network as a concurrent, distributed system  insightful or insanity? Pr Muffy Calder (Department of Computing Science, University of Glagow) Yes, this really is a computer science seminar! In this talk I will consider how theories and tools from Computing Science can be used to model and reason about biochemical pathways. I will consider the ERK signalling pathway as an example and show how we can use the Markovian process algebra PEPA to develop and analyse a number of novel, predictive models. I will discuss how these compare with traditional biochemical models, what the biologists say about them, and the implications for computing science. No prior knowledge of biochemistry nor PEPA will be assumed. NonInterference for Weak Observers David Clark (King's College London) Language based security properties are experiencing a resurgence of attention as part of the more general interest in security. These properties are aimed at curtailing the presence of unwanted flows and related covert channels in programs. One much studied confidentiality property is noninterference (NI) which seeks to guarantee that the activities of high confidentiality users of the program cannot be observed by low confidentiality users. Giacobazzi and Mastroeni's 2004 POPL paper, "Abstract NonInterference: Parameterizing NonInterference by Abstract Interpretation" indirectly posits what we call a "weak observer": someone who is unable to "see" all the low confidentiality data available. We characterise a subclass of their abstractions of the observer by using relations and show that the presence of unsensed, nonconfidential information is experience by the weak observer as nondeterminism. We then demonstrate the obvious: that a possibilistic definition of NI is inadequate and propose our own, probabilistic definition. We show its relationship with Gray's prestrictiveness and sketch how it might be weakened to measure flows of secret information using information theory. This is joint work with Sebastian Hunt and Pasquale Malacaria Adjunction Models For CallByPushValue With Stacks Dr Paul Lévy (The University of Birmingham) Callbypushvalue is a "semantic machine code", providing a set of simple primitives from which both the callbyvalue and callbyname paradigms are built. We present its operational semantics in the form of a stack machine, and see how this machine suggests a term judgement of stacks. We then see that CBPV, incorporating these stack terms, has a simple categorical semantics based on an adjunction. We describe this semantics incrementally. First, we introduce locally indexed categories and the opGrothendieck construction, and use these to give the basic structure for interpreting the 3 judgements: values, stacks and computations. Then we look at the universal property required to interpret each type constructor. We define a model to be a strong adjunction with countable coproducts, countable products and exponentials. We see a wide range of instances of this structure: we give examples for divergence, storage, erratic choice, continuations, games (with or without a bracketing condition) etc., in each case resolving the familiar strong monad (as advocated by Moggi) into a strong adjunction. 

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