• People
• Events
• Research

Lab Lunch Talks 2007

Archive: 1994 · 1995 · 1996 · 1997 · 1998 · 1999 · 2000 · 2001 · 2002 · 2003 · 2006 · 2007 · 2008 · 2009

• 11 November Brian Campbell A Random Voting Method

  Many members of LFCS attended Eric Maskin's recent lecture on voting methods and desirable properties for them. By way of contrast I would like to talk about the rather strange and complex procedure used for centuries to elect the Doge of the Republic of Venice. The properties described by Maskin are immediately ruled out because the procedure uses random lots. However, Mowbray and Gollmann (whose work the talk is based on) have established that the protocol nevertheless provides several useful (and reassuring) properties. They even suggest this voting method may be useful for computer protocols...

• 27 November Xibei Jia Improving Data Quality with Conditional Functional Dependencies

  Real life data is often dirty. It has been reported that 41% of data warehousing projects fail mainly due to data quality problems. There has been recent work on constraint based techniques for improving data quality which capture the errors in data as violations of constraints. In this talk, a new class of constraints introduced in our data cleaning project --- referred to as Conditional Functional Dependencies (CFDs) --- will be presented. Aiming at characterising the consistency of data, CFDs extend traditional Functional Dependencies (FDs) by incorporating bindings of semantically related values. The applications of CFDs in detecting and removing inconsistencies in data will also be reported.

• 20 November David Aspinall Hiproofs for Proof General

  postponed to a later date

• 13 November Jaroslav Sevcik The Java Memory Model

  The operational semantics of multi-threaded Java is not an interleaved semantics. Instead, the Java Language Specification defines a more flexible semantics called the Java Memory Model (JMM). In my talk, I will overview main motivations for having a relaxed memory model, and discuss how the JMM meets its design goals.

• 6 November Alan Bundy Where's My Stuff? An Ontology Repair Plan

  Appropriate representation is the key to successful reasoning. Hence, if intelligent agents are to cope with changing goals in a changing environment, they must be able to adapt their representations, i.e., to detect that a current representation is inadequate, to diagnose its shortcomings and to repair it. In this talk we address the most basic kind of representational shortcoming: inconsistency. We focus on how certain kinds of inconsistency can be repaired using a repair plan that we entitle “Where's My Stuff?”. We apply this repair plan manually to four examples from the domain of Physics. In each case an inconsistent ontology is repaired into a consistent one. The Physics domain has the advantage that many faulty ontologies have been recorded by historians of science, together with the evidence that identified their faults and the ontological repairs that were proposed to mend them. These records provide plenty of data for developing and evaluating ontology repair plans.

• 30 October Jane Hillston Centre for Systems Biology at Edinburgh

  As some of you may know, Edinburgh was successful last year in a bid to BBSRC to establish one of six regional centres for research in systems biology. Gordon Plotkin, Igor Goryanin and I were among the PIs for the application. The centre is now starting to be active, with the recruitment of a significant number of postdoctoral researchers. It is currently housed in a designated area within Darwin and a dedicated building is to be built, starting next year. In this talk I will aim to give an overview of the planned activities of the centre, including giving information about ways in which people who are interested may be able to get involved.

• 23 October Marco Stenico Spatial models in epidemiology

  Space plays a crucial role in epidemiology. In this talk I will discuss some examples of epidemiological models and I will present some classical representations of space.

• 16 October Phil Wadler Well-typed programs can't be blamed

  We show how contracts with blame fit naturally with recent work on hybrid types and gradual types. Unlike hybrid types or gradual types, we require casts in the source code, in order to indicate where type errors may occur. Two (perhaps surprising) aspects of our approach are that refined types can provide useful static guarantees even in the absence of a theorem prover, and that type dynamic should not be regarded as a supertype of all other types. We factor the well-known notion of subtyping into new notions of positive and negative subtyping, and use these to characterise where positive and negative blame may arise. Our approach sharpens and clarifies some recent results in the literature.

  [Joint work with Robby Findler.]

• 9 October Alex Simpson Transformations on random streams

  A random stream is a stream of discrete data generated by a sequence of stochastic events (e.g. by repeatedly tossing a fair coin). This talk will address the question: which transformations on streams preserve randomness? If time permits, I may also discuss briefly how this kind of question gives rise to a notion of "random space" with an associated "random geometry".

• 2 October Vasileios Vasaitis The Type System of C++

  C++ is a mostly overlooked language in the School of Informatics, where Java is prevalent these days for imperative / OO programming. It is also frowned upon inside LFCS, probably because of its bulky and complicated core and therefore its unsuitability for formal reasoning about programs.

  Nevertheless, over the years C++ has developed a very advanced type system, rivalling even functional programming languages in its capabilities. Central to that is the by now indispensable feature of templates, a powerful compile-time metaprogramming framework, with uses ranging from simple parametrized types to extending the language in surprising ways. This talk will present the C++ type system, focusing on the role of templates and also presenting a few of their uses.

• 25 September Allan Clark

  Performance measurement specifications using stochastic probes in Pepa

  This will be an amalgamation of a talk I gave in June at Pepa Club and one I gave in late July at the Pasta workshop. I will begin with a very brief overview of the Pepa process algebra, I will then define what exactly a performance measurement probe is. I will then progress to describing our regular-expression-like language for specifying performance probes and of course give some examples. Finally I will give an insight into my implementation of probes within the Imperial Pepa Compiler.

• 11 September Jorge Branco Aires

  "Exception Aware" Type Systems

  Keeping track of exceptions that might be raised during the execution of a program is a task that might be made simpler with the introduction of type systems that are 'exception aware'. In this talk it will be presented an 'error annotated' type system for call by value languages with raising and handling of exceptions, as well as its semantics based on deterministic concrete data structures and sequential algorithms and how they shaped the definition of the type system itself. This approach aims to keep the rules simple and only two annotations per type are used - one for raising and another for handling of exceptions, (contrasting with other systems which use one annotation per arrow) - while still being powerful enough to deal with higher order functions. No previous knowledge on the subject should be needed as the topic will be presented at a fairly high level.

• 4 September Marek Kwiatkowski

  The Topology of the Possible

  The most common generic model of biological evolution is the so-called fitness landscape: every genotype is assigned a numerical value representing the fitness of the resulting organism. The evolution through natural selection can then be seen as "hill-climbing" -- the fitness increase and so the organism moves "higher" in the landscape. Unfortunately, this model largely ignores mechanisms essential to the understanding of biological robustness and evolvability.

  Around 2000, a group of theoretical biologists affiliated with the Santa Fe Institute showed how to use topologies to give an alternative generic model to address this drawback. In my talk, apart from explaining all non-CS terms from the previous paragraph, I am going to present their insights. Their model is especially applicable to the evolution on the molecular level, and so the construction is going to be performed on the example of RNA structures and their evolution.

  The talk is going to be medium-long (around 30min) and fairly high-level (i.e. the construction is not going to be performed in detail).

• 28 August Joseph Spadavecchia

  Multidimensional Indexing of Structured Peer-to-Peer Networks

  Most relational databases use special data structures called indexes to improve query performance. The primary job of an index is to provide fast access to data stored on disk through various kind of queries. Traditionally, indexes and their data are stored on a single computer, i.e., the database server, with certain parts stored in memory. Under this setting, indexing has been studied extensively and a variety of indexes have been developed for various types of data.

  Recently, however, with the widespread availability of inexpensive computers and expansion of the Internet, a need has arisen for indexing data that is spread over many, possibly millions, of independently operated computers. Common applications requiring such indexes include, cooperative storage systems, distributed web-caches, peer-to-peer search engines and file-sharing applications.

  The focus of this talk will be to present my work on indexing for a certain class of large-scale distributed systems called structured peer-to-peer networks. In this talk I will first present my area of research and thesis topic followed by an overview of the state-of-the-art. I will then summarise my work on a decentralised index for structured peer-to-peer systems and conclude with some future work directions.

• 14 August James Matthews

  Sampling Perfect Matchings in a Restricted Class of Bipartite Graphs

  Some statistical tests require us to uniformly sample permutations of a set of data, where the allowable positions of each datum may be restricted. This can be shown to be equivalent to sampling perfect matchings in a restricted class of bipartite graphs, where each row contains a single contiguous block of 1s. Existing Markov chain algorithms sample from perfect and near-perfect matchings, with the fastest current approach achieving O(n^7 log^4 n) runtime. Diaconis, Graham and Holmes proposed a new Markov chain that samples directly from perfect matchings in this class of graphs. I will show that this new chain is not rapidly mixing in the case where each row contains a single block of 1s. However, there is a further restriction to the class of graphs, for which the chain can be shown to mix in sub-exponential time. For a very restricted class of graphs where the 1s in each row of the adjacency matrix are aligned to the left, the chain is rapidly mixing, but it is straightforward to sample exactly in this case.

• 31 July William Stirton

  Some Issues About how to Prove Normalizability of Typable Classes of Lambda Terms

  I will start by describing a situation which I presume computer scientists often find themselves in. You have a set of rules which assign types to lambda terms and you want to show that the terms typable by these rules are all normalizable. More than that, you would probably also like to find an upper bound to the class of functions represented by the terms. As is well known, this task is closely related to that of proving normalizability of an ordinary theory (in natural deduction style) or cut elimination (if it is in sequent style). If you want to answer the second question, you will want what proof theorists call an "ordinally informative" proof of normalizability resp. cut-elimination. I will review some of the tools available and float some questions, opinions and conjectures. I will argue that Schwichtenberg's answer to the question "How long can the longest reduction sequence of a typed lambda term possibly be?" has an importance for proof theory which has perhaps not been sufficiently appreciated. NB: while this lecture is designed mainly for people who have some interest in proof theory and/or typed lambda calculi, I certainly will not assume any deep expertise.

• 17 July David Harel

  Can Programming be Liberated, Period?

  This brief talk will be about a nontechnical dream/vision paper I am finishing these days, whose title is a play on that of John Backus' Turing Award Lecture (and paper). I will propose that --- or rather ask whether --- programming can be liberated from its three "straightjackets": having to produce an artifact in some language, having to actually produce two separate ones (the program and the set of requirements) and then to compare the two, and having to program each piece/part/object separately.

• 10 July Sam Lindley

  Typed Lambda Calculi and Applications (TLCA) 2007

  Trip report.

• 3 July Michael Smith

  Stochastic Bounds and Abstract Interpretation of Stochastic Process Algebra

  When modelling the performance characteristics of computing systems, we often use stochastic processes as an abstraction. In particular, Markov chains are often used, since they can be solved analytically. The main problem, however, is that the state space can quickly grow too large to handle, particularly when we have components running in parallel.

  A common technique for reducing the size of a Markov chain is aggregation, where states with similar behaviour are approximated by a single state. Unfortunately, exact aggregation is a very strict condition, and if we try to approximate this, it is very difficult to reason about the errors involved. Stochastic bounds allow us to construct an upper and lower "bound" of the Markov chain, each of which can be exactly aggregated, so that we can solve each of them and have an exact bound on the solution of the original chain.

  In this talk, I will present an introduction to stochastic ordering and stochastic bounds, and then show how this can be applied to the stochastic process algebra PEPA. The idea here is one of abstract interpretation - namely we wish to construct a bound for each sequential component independently, and then compose these to obtain a bound on the entire system. Finally, I will talk about the limitations of this technique (most importantly, relating to the tightness of the bounds), and some thoughts on the next steps.

• 19 June Ezra Cooper

  Optimally Auctioning CPU Time

  One way to allocate resources (like CPU time) on a computational grid is using market mechanisms, running a quick auction at each host whenever a new "agent" arrives. I'll describe some market mechanisms and planning strategies (developed by Jonathan Bredin) that hosts and agents can use to optimize their utility. This market-based approach to resource control might be an interesting contrast (or complement) to an approach based on proof-carrying code.

• 12 June Perdita Stevens

  A Smidgen of Group Theory

  Once upon a time, in a country far away, I used to be an algebraist. Lately I've been engaged closer to the coal face of software engineering. For example, I'm interested in model transformations: situations in which a model of some aspect of a software system, such as a design expressed in UML, is automatically transformed into another model, such as a database schema. This gets more interesting when you want bidirectional transformations: a change made in either model should be able to be propagated to the other. What formalisation gives sanity as well as the flexibility needed in practice? How can we build transformations compositionally, taking account of the structure of the models? In trying to understand these issues - and especially, to understand the relationship between model transformations and the work done by Benjamin Pierce and colleagues on bidirectional programming - I stumbled upon bits of group theory that I thought never to meet again, such as short exact sequences, semidirect products and wreath products.

  This talk will be in the Spirit of Lab Lunch - at least, it will be informal: short may be harder, but I'll try. I'll probably focus on the group theory, and handwave at the applications (i.e. you will not have to be able to expand UML, OMG, QVT etc.). Benjamin Pierce, who will be visiting during this week, will be giving a proper talk on Friday, for those who would like to hear more.

• 5 June Michael Smith

  The Game of Go

  Go (Igo in Japanese, Wei chi in Chinese, and Baduk in Korean) is widely believed to be the oldest game in the world, originating 4000 years ago in China. The essence of the game has changed very little over this time, the objective being to surround "territory" by placing black and white stones on a grid (usually 19x19). Unlike games such as chess, in which a single battle takes place, a game of Go will involve multiple battles across the board, all taking place simultaneously. These battles in turn are not independent, as certain situations called "ladders" and "ko fights" involve the whole-board situation in addition to local fighting.

  In this talk, I will explain the rules of Go (which are surprisingly simple), and introduce some of the most important concepts, largely by demonstration. The aim is not to teach you how to play (which can only be done by much practice), but to encourage you to start playing. In particular, there is an active group of Go players in Edinburgh. Finally, I will mention briefly some of the Go-playing programs that exist, and the challenges that the game poses to the AI community.

• 15 May Michael Fourman

  Perspectives on Action

  Quantales provide a categorical setting for action algebras. Treatments of the frame problem in AI introduce a notion of local changes, that affect only a restricted set of fluents.. I will discuss the structures needed to introduce notions of fluents and local changes in the context of quantales.

• 8 May Robert Atkey

  TYPES 2007 Conference

  Trip report.

• 1 May Kyriakos Kalorkoti

  Groups, Machines and p-adic Numbers.

  There has been interest recently in groups with decision problems that are "almost" solvable. In this talk I will outline the construction of a finitely presented group with solvable word problem but unsolvable conjugacy problem. However the instances of unsolvability are a fast vanishing fraction of the total (in a precise sense). Perhaps the most interesting aspect from the computer science view point is that the analysis led to the notion of machine configurations that consist of pairs of p-adic numbers and a notion of a many-fold computation step. The talk will be at a fairly high level with technical details avoided as far as possible.

• 24 April Julian Bradfield

  British Colloquium for Theoretical Computer Science and British Mathematical Colloquium

  Trip reports.

• 20 March Dominik Wojtczak

  PReMo - an Analyzer for Probabilistic Recursive Models

  I would like to present a tool called PReMo that I have developed in Java. PReMo can be used to compute termination probabilities and expected termination time of Recursive Markov Chains, Recursive Simple Stochastic Games and Stochastic Context-Free Grammars. First I will present some background knowledge behind Recursive Markov Chains and describe a fundamental non-linear system of equations whose Least Fixed Point gives us the termination probabilities we are after. After that I will describe some standard numerical algorithms implemented in PReMo used to find this fixed point, show some experimental results how these algorithms compare in practice and in the end give a live demonstration of PReMo.

  This work will appear at Tools and Algorithms for Construction and Analysis of Systems (TACAS) 2007.

• Michael Smith

  Stochastic Modelling of Communication Protocols from Source Code

  Lots of people build performance models of systems - not only for the fun of it, but to calculate some property of the real system. But how do we know that a given model has anything to do with the system it's supposed to describe? The approach that I will talk about is to derive a stochastic model directly from the source code of the system; in this case, communication protocols. The key idea is that we have to carry around an abstract environment of the program's data variables in order to determine the probability of control flow decisions being taken. I will illustrate the approach with an example analysis of a simple protocol.

  This work will appear in Quantitative Aspects of Programming Languages (QAPL) 2007.

• 20 February Ian Stark

  Contemplating the Size of Some Rectangles

  This lab lunch talk is more in the way of a practical: Marije has a supply of tape to stick onto the 2510 floor, and I propose we use it to mark out the expected dimensions of offices in the Informatics Forum. Extensions could include testing out furniture arrangements, and reflecting on possible layouts for multiple occupants.

  I have no information to bring beyond the plans already published on the web, but I will try to get the 3d model up and running for people to browse and attempt walkthroughs.

• 13 February Sibylle Froeschle

  When is Secrecy Decidable?

  This will be a light talk, which can be seen as a taster for the TPG course 'Formal Analysis of Cryptographic Protocols' due to start on Thursday (15th February) at 3pm in 2509.

  The hope for employing complete automatic methods to validate the security of cryptographic protocols has been thwarted by the fact that most security properties such as secrecy have turned out to be undecidable. On the other hand, one could argue that the undecidability proofs exhibited so far do leave room for positive results: most of these proofs exploit properties of the formal models used to represent protocols rather than characteristics possessed by 'realistic protocols'. In this talk I will motivate and identify several open problems in the area.

• 6 February Kousha Etessami

  Multi-Objective Model Checking of Markov Decision Processes

  I'll give a very casual (whiteboard) talk describing the topic of the title (hopefully without too much technical stuff). Along the way, I'll touch on concepts like "approximate Pareto curves", "randomized strategies" , "stochastic flow equations", and inevitably, omega-automata. Applications to assume-guarantee compositional reasoning for probabilistic systems may also be discussed, if I find time. This describes joint work with M. Kwiatkowska, M. Vardi, and M. Yannakakis, that will appear at TACAS'07.

• 30 January David Harel

  Towards an Odor Communication and Synthesis System

  We propose a setup for an odor communication and synthesis system. The applications of such a scheme are essentially limitless: from e-commerce, games and video via the food and cosmetics industry to medical diagnosis. Our approach enables an output device --- the whiffer (a sort of smell printer) --- to release an imitation of an odor read in by an input device --- the sniffer (a sort of smell camera, e.g., an electronic nose) --- upon command. The heart of the system is the novel mathematical/algorithmic scheme that makes the scheme feasible. We have been carrying out a large amount of work researching and developing some of the components that constitute the scheme, many of which have to do with the understanding and analysis of electronic nose space, including odor identification and classification and mixing. In this short talk I will be able to report only on very few of these results.

Archive: 1994 · 1995 · 1996 · 1997 · 1998 · 1999 · 2000 · 2001 · 2002 · 2003 · 2006 · 2007 · 2008 · 2009