Computer Science Seminars and Short Courses

Srinivasa Rao Satti (Seoul National University, Korea )
Fri, July 22, 14:00 in ATT LT3 (Host: Rajeev Raman)

We consider the problem of representing integers in close to optimal number of bits to support increment and decrement operations efficiently. We study the problem in the bit probe model and analyse the number of bits read and written to perform the operations, both in the worst-case and in the average-case. We propose representations with different trade-offs between the space used and the number of bits probed. We also study the problem of representing integers to support addition and subtraction operations. We propose a representation that uses n + O(log n) bits to represent integers in the range [0, ... ,2^n - 1] which supports addition and subtraction operations, improving the space complexity of an earlier representation by Munro and Rahman [Algorithmica, 2010]. We also show various trade-offs between the operation times and the space complexity.

This is a joint work with Gerth S. Brodal, Mark Greve and Vineet Pandey

Lutz Schröder (Bremen, Germany)
Fri, June 24, 14:00 in ATT LT3 (Host: Alexander Kurz)

Modal logic is currently one of the most successful logical formalisms in computer science, in particular through its role as the basis for temporal logics on the one hand, and for description logics on the other hand. While modal logics are standardly equipped with a relational semantics, many modes of expression found both in knowledge representation and in the more detailed modelling of reactive systems, in particular where these involve uncertainty or multiple agents, require substantial extensions or modifications of relational semantics. Coalgebraic logic serves as a unified semantic and algorithmic framework for such modalities. We give an introduction to coalgebraic logic and then present a specific result on timed-out tableaux for coalgebraic fixed point logics (joint work with Yde Venema) in more detail.

Pierre Clairambault (Bath)
Fri, 17 June, 14:35 in ATT LT3 (Host: Andrzej Murawski)

We investigate the problem of type isomorphisms in a programming language with higher-order references. We first recall the game-theoretic model of higher-order references by Abramsky, Honda and McCusker. Solving an open problem by Laurent, we show that two finitely branching arenas are isomorphic if and only if they are geometrically the same, up to renaming of moves (Laurent's forest isomorphism). We deduce from this an equational theory characterising isomorphisms of types in a finitary language L_2 with higher order references. We show however that Laurent's conjecture does not hold on infinitely branching arenas, yielding a non-trivial type isomorphism in the extension of L_2 with natural numbers.

Thomas Jansen (Cork, Ireland)
May 27, 14:00 in ATT LT3 (!!) (Host: Igor Razgon)

Evolutionary algorithms are nature-inspired general randomised search heuristics. They are applied successfully for many different tasks, typically when no good problem-specific algorithm is available. The analysis of evolutionary algorithms aims at understanding the fundamental working principles in a precise way, exhibiting limitations, and guiding the way to improvements. We consider as an example mutation and the influence of the mutation probability on the optimisation time considering the class of strictly monotone pseudo-Boolean functions. These functions are a proper super-set of the class of linear pseudo-Boolean functions and a proper super-set of the class of unimodal pseudo-Boolean functions. For linear functions over n bits it is known that each mutation probability of size c/n leads to efficient optimisation. For unimodal functions it is known that no mutation probability can achieve that. We demonstrate that strictly monotone functions are in between in the sense that if c a sufficiently small constant the optimisation is efficient but becomes very inefficient if c is a larger constant. We discuss consequences for the choice of the mutation probability.

Prakash Panangaden (McGill, Canada)
May 13, 14:00 in RAT LT (Host: Alexander Kurz, Andrzej Murawski)

In this talk we consider the problem of representing and reasoning about systems, especially probabilistic systems, with hidden state. We consider transition systems where the state is not completely visible to an outside observer. Instead, there are observables that partly identify the state. We show that one can interchange the notions of state and observation and obtain what we call a dual system. The double dual gives a minimal representation of the behaviour of the original system. We extend this to nondeterministic systems and to probabilistic transition systems and finally to partially observable Markov decision processes (POMDPs). In the case of finite automata restricted to one observable, we obtain Brzozowski's algorithm for minimizing finite-state language acceptors. I will explain the co-algebraic reason why this works at the end. This project began with joint work with colleagues from McGill especially Doina Precup and Chris Hunt. The recent co-algebraic understanding is joint work with Clemens Kupke and Nick Bezhanishvili.

Jinyun Xue (Jiangxi Normal University (JXNU), China)
May 9, 10:00 in KE LT2 (Host: Jose Fiadeiro)

It is a challenging task of computer scientists for increasing the reliability of software and efficiency of developing software. For answering the challenge, we are developing the PAR method and its supporting platform, called PAR platfor, that is a long-term research project supported by a series of research foundations of China. PAR method and PAR platform consists of PAR programming methodology, specification and algorithm describing language Radl, abstract programming language Apla, a set of rules for specification transformation and a set of automatic transformation tools of algorithm and program. PAR provides powerful generic structures that support convenient generic programming and the methodology that supports formal derivation of executable algorithmic programs from their formal specification. PAR can be used to develop correct application program that access to database and to develop software components with high reliability.

In this talk, I will pay main attention on outlining the components and main functions of PAR as well as innovative techniques in developing PAR. After that, I will present some new research goals that is to add some new language mechanism to Radl and Apla. The goals are the center tasks of two research projects that were proposed by Prof. Jose Fiadeiro and me and supported by the Chinese Ministry of Science and technology and the NSF of China.

Conor McBride (Strathclyde)
Fri Mar 25, 14:00 in RAT LT (Host: Alexander Kurz, Tadeusz Litak)

Circular programs always make my head spin, and sometimes my computer too. Lazy evaluation allows us to trade in data which do not yet exist, in the hope that they can be computed just in time. If an apparently circular program does not, in fact, have cyclic data dependencies, it will work! However, it is only too easy to write well-typed programs which consume data before they are produced and spiral into a black hole. This talk presents a typed approach to circular programming, abstractly modelling relative time, ensuring that the present does not depend on the future. Classic perplexing examples, such as repMin, and even the breadth-first tree-labelling algorithm of Jones and Gibbons are explicable in this setting, with a minimum of fuss. There is more than a hint of a connection with modal logic, which I should like to learn more about if time and the audience permit.

Ulrich Schöpp (Munich)
Fri, Mar 18, 14:00 in RAT LT (Host: Alexander Kurz, Frank Nebel)

In game semantics computation is modelled by question and answer dialogues. While dialogues are most often studied as abstract mathematical objects, there are also examples where it is interesting to use such dialogues for actual computation. Ghica implements dialogues by digital circuits and is thus able to synthesise circuits from programs in a higher programming language. Another example where computation with dialogues is natural can be found in the context of programming with data that is too large to fit into memory. In work on game semantics it is standard to abstract the concrete details of question/answer dialogues, not least because these details can sometimes be complicated. In this talk I will show how the implementation of dialogues can similarly be aided by programming language constructs for metaprogramming. With a view to intended applications like the ones mentioned above, the emphasis lies on metaprogramming for weak languages. I will also consider the implementation of dialogues in languages with computational effects such as state or non-determinism.

Clemens Ley (Oxford)
Fri, Mar 11, 14:00 in RAT LT (Host: Alexander Kurz, Emilio Tuosto)

In algebraic language theory, certain algebraic objects, primarily monoids, are used to analyze the structure of string and tree languages. A fundamental result states that a language is regular iff it is accepted by a finite monoid. Subclasses of regular languages, such as star-free languages correspond to natural classes of finite monoids. Most prominently, Schützenberger, McNaughton, and Papert showed that a regular language is first order definable iff it is star-free iff it is accepted by an aperiodic monoid.

The study of data languages -- languages over an infinite alphabet -- is motivated by applications in verification and XML processing. In this talk I will report about a recent extension of algebraic techniques to the study of data languages. A class of infinite monoids, finite-orbit data monoids, has been proposed by Bojanczyk. We present a logic, called rigidly-guarded monadic second order logic, that defines exactly the languages accepted by finite-orbit data monoids. A theorem akin to Schutzenberger's Theorem also carries over to data languages: We show that a language is definable in rigidly-guarded first order logic iff it is accepted by an aperiodic data monoid.

Olivia Caramello (Cambridge)
Thu, Mar 10, 16:00 in MAB 1.19 (Host: Alexander Kurz, Daniela Petrisan)

Bartek Klin (Cambridge/Warsaw)
Fri, 4th March, 14:00 in RAT LT (Host: Alexander Kurz)

First I will show how a simple categorical understanding of deterministic automata in the spirit of Arbib and Manes, when instantiated in the category of nominal sets as studied by Gabbay and Pitts, yields a useful model of finite computation on infinite alpabets, closely related to HD-automata of Pistore and others, and enjoying better properties then Finite Memory Automata of Francez and Kaminski. These are then generalized to cater for alphabets with structure (such as an order or a graph) that can be checked upon by automata. In the process, the theory of nominal sets needs to be generalized to arbitrary groups of permutations rather than symmetric groups. A particularly well behaved class of alphabets arises from the model-theoretic study of Fraisse limits.

Private local memory and shared memory in multi-core systems causes headaches: programs have concurrency errors (races); cache effects expose the fiction of random access memory; and private local memory requires explicit inter-processor data transfers. We show how an intuitive type system can enforce data isolation between tasks. This eliminates data races and also allows a compiler to freely allocate tasks to processors without changing program meaning and with increased performance predictability.

Ontologies have recently been used to support software development activities. Ontologies are rooted in description logics and consequently support formality and rigour in development of software, but ontologies are also conceptual modelling frameworks close to common software modelling notations such as UML.

Based on a framework for ontology-driven software development, we investigate the potential, but also the limitations of using ontologies for software modelling and reasoning. We specifically look at software architecture design and service-oriented architectures, focussing on architecture patterns, service composition and behaviour modelling. At the core of the solution are extensions and adaptions of description logics to encompass process behaviour and process-based patterns as abstractions.

Nick Benton (Microsoft Research)
Feb 11, 14:00 in RAT LT (Host: Tom Ridge, Alexander Kurz)

Developers turn coffee into programs, whilst mathematicians turn it into proofs. Amazingly, proofs and programs are not just made from the same stuff, but there's a strong sense in which they actually *are* the same stuff. The modern understanding of proofs, programs, and the correspondence between them, is one of the most significant intellectual developments of the 20th century. That understanding is now embodied in a radically new kind of language and software tool that could revolutionize both mathematics and software development in the 21st century.

Semester 1, 2010/11

Seminar programme

Seminar details

Ranko Lazic (Warwick)
Fri Dec 10, 14:00 in BEN LT1 (Host: Alexander Kurz, Andrzej Murawski)

Even without continuous phenomena, words and trees over finite alphabets are sometimes insufficiently detailed models. A prominent example is processing semistructured data, which may involve attribute values from infinite domains. With such a motivation, several formalisms for reasoning about words and trees with infinitary data have recently been studied, using a variety of techniques. The emerging landscape is interesting, but careful navigation is required for avoiding undecidability and very high complexity.

James Cheney (Edinburgh)
Wed, 8 Dec, 4pm in ENG LT1 (Host: Alexander Kurz, Tadeusz Litak)

Over the last 10 years, members of the database, programming language and Web communities have developed a nice, purely functional (in parts) query language for tree-structured data called XQuery, including a formal semantics that is a (non-normative) W3C standard. Many people are now intent on adding imperative features so that tree-structured data can also be updated. Doing so can easily damage the existing advantages of XQuery. I’ll present some work on a clean, but not very expressive language called FLUX , and contrast it with the semantics of the W3C update proposal currently under development, focusing on the issue of typechecking. Time permitting I will also discuss more recent work on static analysis and optimization for the W3C language.

Axel van Lamsweerde (Universite catholique de Louvain, Belgium)
postponed in (Host: Jose Fiadeiro)

The effectiveness of MDE relies on our ability to build high-quality models. This task is intrinsically difficult. We need to produce sufficiently complete, adequate, consistent, and well-structured models from incomplete, imprecise, and sparse material originating from multiple, often conflicting sources. The system we need to consider in the early stages comprises software and environment components including people and devices.

Such models should integrate the intentional, structural, functional, and behavioral facets of the system being developed. Rigorous techniques are needed for model construction, analysis, and evolution. They should support early and incremental reasoning about partial models for a variety of purposes, including satisfaction arguments, property checks, animations, the evaluation of alternative options, the analysis of risks, threats and conflicts, and traceability management. The tension between technical precision and practical applicability calls for a suitable mix of heuristic, deductive, and inductive forms of reasoning on a suitable mix of declarative and operational models. Formal techniques should be deployed only when and where needed, and kept hidden wherever possible.

The talk will provide a retrospective account of our research efforts and practical experience along this route, including recent progress in model engineering for safety-critical medical workfows. Problem-oriented abstractions, analyzable models, and constructive techniques are pervasive concerns.

Henrik Nilsson (Nottingham)
Fri, 26 Nov, 14:00 in BEN LT1 (Host: Alexander Kurz, Tadeusz Litak)

Equational models of physical phenomena and systems is essentially non-causal: the equations simply state the relation among the involved entities. However, solving such equations, for example, predicting the behaviour of a system through simulation, has traditionally required a manual re-formulation into causal form, allowing the "known" entities to be used for computing the "unknowns". This causal re-formulation can be very cumbersome, especially for large models. This has led to the development of modelling and simulation languages that directly support a non-causal formulation, obviating the need for manual causalisation. This also turns out to give additional important methodological and modularity benefits. However, the current industrial-strength non-causal modelling and simulation languages have a number of limitations, notably when it comes to describing hybrid systems: systems that exhibit both continuous-time and discrete-time characteristics. In this talk, I'll outline a novel approach to non-causal modelling and simulation of hybrid systems, called Functional Hybrid Modelling (FHM), aimed at mitigating some of these limitations. As the name suggests, it draws from functional programming; in particular, it can be seen as a generalisation of Functional Reactive Programming (FRP), which allows very general hybrid systems to be described, except only causally.

Nikos Tzevelekos (Oxford)
Fri, 19 Nov, 14:00 in BEN LT1 (Host: Alexander Kurz)

What is a basic automata-theoretic model of computation with names and fresh-name generation? We introduce Fresh-Register Automata (FRA), a new class of automata which operate on an infinite alphabet of names and use a finite number of registers to store fresh names, and to compare incoming names with previously stored ones. These finite machines extend Kaminski and Francez’s Finite-Memory Automata by being able to recognise globally fresh inputs, that is, names fresh in the whole current run. We examine the expressivity of FRA’s both from the aspect of accepted languages and of bisimulation equivalence. We establish primary properties and connections between automata of this kind, and answer key decidability questions. As a demonstrating example, we express the theory of the pi-calculus in FRA’s and characterise bisimilarity by an appropriate, and decidable in the finitary case, notion of bisimilarity in these automata.

Neil Ghani (Strathclyde)
Fri, 12 Nov, 14:00 in BEN LT1 (Host: Alexander Kurz)

We all learned about induction for proving properties of natural numbers at school. But what about other data types such as lists - do they have induction principles? And what exactly are properties and can we use induction for different notions of properties. Finally, if we work in categories other than the category of Sets, do we still have induction principles?

In this talk I'll show that, indeed, we can have induction principles parameterised by the category we work in , the data type we are interested in and the notion of property under consideration. These results arise from a very beautiful picture of induction if one will willing to consider the topic within a fibrational setting.

In this overview talk I will mention three types of terms (finite, rational and infinite) and show how they arise naturally when considering recursive equational specification. Moreover, their algebraic theories all enjoy universal properties, distinguishing them as free theories among theories of a certain type.

The results mentioned in this talk have been obtained in cooperation with Jiri Adamek and Stefan Milius.

Ann Blandford (UCL)
Fri, Oct 29, 14:00 in BEN LT1 (Host: Jose Fiadeiro, Effie Law)

Widely used interactive medical devices such as infusion pumps pose interaction difficulties. These include difficulties in programming, interaction and socio-technical design, all of which may result in untoward incidents. These difficulties have rarely been a focus for study: they are effectively invisible. In this talk, I will discuss what is currently known about the design and use of interactive medical devices and outline ways of improving the designs to better support the needs of clinicians and patients.

Reiko Heckel (Leicester)
Fri, Oct 22, 14:00 in BEN LT1 (Host: Jose Fiadeiro)

When using models to understand observed natural, social or technical processes (as opposed to designing them), we are interested in abstraction as the common direction of model development. Starting from a detailed model or observation, some of the features are ignored in order to simplify and reduce the model, for example with a view to improving our capacities for analysis.

In Computer Science, a variety of methods and tools have been developed to define modelling languages and support the transformation and analysis of models. It is the aim of this talk to show how such methods can be applied to Biological Membrane Models, i.e., models of hierarchical cellular systems with local interactions and mobility.

Specifically, we will use stochastic graph transformation systems to model membrane systems, analyse quantitative properties and develop a method of abstraction based on "forgetting" all instances of types we want to abstract from. This yields an abstraction function on states which extends to rules and transformations in the system, thus preserving the behaviour.

We will also discuss how can extend this notion of abstraction to stochastic systems, by defining a statistical measure of distance based on correlations between frequencies of rule applications. Such a measure can be used to assess the quality of an abstraction through stochastic simulation of the two systems.

We illustrate our concepts by a generic model for infection, recovery and death of cells, using features of membrane systems in a graph representation.

Peter D Mosses (Swansea)
Fri, Oct 15, 14:00 in BEN LT1 (Host: Jose Fiadeiro)

New programming languages and domain-specific languages (DSLs) are continually being introduced, as are new versions of existing languages. Each language needs to be carefully specified, to determine the syntax and semantics of its programs - independently of any particular implementation or machine architecture.

If one has to start from scratch, it takes a huge effort to give a precise specification of a major new language. However, new languages typically include a large number of constructs from previous languages, presenting a major opportunity for reuse of specification components.

We first consider the modular structure of language specifications, and its consequences for reuse. Then we review various frameworks for specifying syntax and semantics, and assess how well they meet the challenges of language specification based on reusable components.

REFERENCES

P. D. Mosses (2004). Modular structural operational semantics. JLAP, 60-61:195-228. DOI: 10.1016/j.jlap.2004.03.008

P. D. Mosses (2008). Component-based description of programming languages. In Visions of Computer Science, pp. 275-286. BCS. URL: http://www.bcs.org/server.php?show=ConWebDoc.22912

P. D. Mosses and M. J. New (2009). Implicit propagation in structural operational semantics. In Proc. SOS 2008, ENTCS 229(4):49-66. DOI: 10.1016/j.entcs.2009.07.073

A. Johnstone, P. D. Mosses, and E. Scott (2010). An agile approach to language modelling and development. Innovations in Systems and Software Engineering 6(1-2):145-153. DOI: 10.1007/s11334-009-0111-6

Recent changes in legislation in the UK have allowed a patient who requires a kidney transplant, and who has a willing but incompatible donor, to be involved in a “pairwise kidney exchange” (i.e., to “swap” their donor) with another patient-donor pair in a similar position. “Pooled donations'' extend this concept to three or more couples in a cyclic manner. NHS Blood and Transplant (NHSBT) run the National Matching Scheme for Paired Donation (NMSPD), which finds pairwise and 3-way exchanges (the latter being pooled exchanges involving three couples) at regular intervals. This matching scheme is based on optimising firstly the number of transplants, and subject to this, the total weight of the transplants, based on a scoring system that incorporates a number of factors including sensitivity, HLA compatibility, age and geographic location. In this talk we describe three computational techniques that we have used in order to construct optimal exchanges for matching runs of the NMSPD between July 2008 and October 2010. The first two of these involve efficient algorithms, based on weighted matching in graphs, to find an optimal set of exchanges and are implemented in C++. The third technique deals with an NP-hard optimisation problem, and uses integer linear programming, using the COIN solver . We present a summary of the results that we obtained for the matching runs, as applied to anonymous data supplied by NHSBT. This is joint work with Gregg O’Malley, Péter Biró and Kirstin MacDonald.

	cms
	HOME	MAP	CONTACT

cms

ABOUT