Lab Lunch Talks 2000

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

5 December Martin Lange <martin@dcs.ed.ac.uk>

A modal fixed point logic with sequential composition
A few years ago Markus Mueller-Olm has introduced FLC, a modal logic with a sequential composition operator. Its syntax is very similar to the modal mu-calculus MMC unlike its semantics, although MMC can be embedded in FLC. FLC's expressive power is a lot greater than MMC's, but its satisfiability problem is undecidable on finite models already. However, the model checking problem is decidable and we will present an idea of how model checking games for FLC might look like and how they can help to understand formulas of FLC.
28 November Don Sannella <dts@dcs.ed.ac.uk>

Progress on EU funding for Global Computation
I have previously reported on discussions in Brussels which have led to allocation of funding for basic research in this area as a so-called "proactive initiative". I have recently been involved in drafting the call for proposals and would like to report what I know about that. I don't expect any further installments in this saga since the actual call will be announced in January.
21 November Paul Anderson <paul@dcs.ed.ac.uk>

A Language for Specifying Large Scale System Configurations
The DICE project is intended to update and unify the infrastructure supporting commodity computing in the Division of Informatics. Part of this infrastructure is the LCFG system developed at DCS for automatically managing configurations of large clusters of machines (//www.dcs.ed.ac.uk/~paul/publications/LISA8_Paper.pdf).
For the next generation of LCFG system, we would like to provide a specialized language for describing these machine configurations which takes into account our experiences with the old system. This talk will present the background problems and some proposed ideas for such a language. Since this is motivated by practical requirements, we would very much like to solict feedback and suggestions for any relevant theoretical foundations or comparable work.
14 November Andrew Sijan <Andrew.Sijan@ed.ac.uk>

Contracts, Licences and Spin-out companies
Commercialisation of ideas and Intellectual Property in Universities is a growing priority area within the Scottish Executive following the recommendations of the government Economy taskforce. The University of Edinburgh represents a source of high technology, high value products and services which can have a significant impact on the Scottish economy and global markets. The presentation is an opportunity to learn and discuss the way in which the University handles commercialisation through Edinburgh Research and Innovation (ERI), the support available and services provided.
31 October Julian Bradfield <jcb@dcs.ed.ac.uk>

Independence-friendly logic
`Independence-friendly logic' is an attempt, chiefly by Hintikka, to bring branching quantifiers (alias Henkin quantifiers) back into mainstream logic, mathematics and even computer science. I'll introduce the ideas of branching quantifiers and Hintikka's logic, and then suggest a natural use in logics for concurrency.
24 October James Brotherston <jjb@dcs.ed.ac.uk>

Isabelle, confluence of beta, and achieving automation
We have recently completed a major proof development in a first-order presentation of the lambda-calculus with one-sorted variable-names, due to Rene Vestergaard. It was done in the Isabelle/HOL proof engine. We will report on our work and, in particular, focus on the issue of proof automation in Isabelle and why it can be difficult to achieve.
17 October Kyriakos Kalorkoti <kk@dcs.ed.ac.uk>

Macaulay's form of the resultant
Consider n homogeneous linear polynomials in n unknowns. When does such a system have a non-trivial zero? The answer is simple and well known to all who have enjoyed a course in linear algebra: precisely when the determinant of the coefficients is zero. Now ask the same question for non-linear polynomials: the answer here is when the resultant polynomial of the system is zero. However the resultant (which is a polynomial with integer coefficients) is much more tricky to get hold of than the determinant. Almost a century ago Macaulay provided an expression for the resultant as the ratio of two determinants. The proof is quite long and there do not seem to be any others available. I will explain how the use of a simple fact about resultants can be used to shorten Macaulay's proof and expose some beautiful structure.
This is not simply an exercise in Mathematical Archaeology; there has been considerable interest in Macaulay's work by people in Computer Algebra as a means of solving systems of equations (e.g., see the recent book "Using Algebraic Geometry" by Cox, Little and O'Shea).
10 October Perdita Stevens <pxs@dcs.ed.ac.uk>

Report on UML2000 and on recent developments in UML standardisation and formalisation
I'll certainly talk about the UML2000 conference: how much I say about the ongoing UML standardisation and formalisation will depend on how much of the latest document I manage to read between now and then! However, the executive summary seems to be that there is a serious ongoing attempt to build UML in a well-defined way on top of something much simpler. The simpler thing, known as MML, is still little to do with the MLs we're more familiar with here -- but it does seem to be going in the "right" direction. I think it would be worth investigating whether MML is amenable to an interesting "proper" formalisation and what that might mean for UML.
3 October Alan Smaill <smaill@dcs.ed.ac.uk>

Linear logic for formation of recursive plans
The suggestion is often made in passing that planning problems, as treated eg for robot planning, could be tackled by using a representation in linear logic. I'll talk about some possibilities in this direction, and how they fit into the construction of recursive plans.
19 September Joanna Tomasik-Krawczyk <joto@dcs.ed.ac.uk>

Approximation of Generalised Semi-Markov Processes by Markov Chains
Amalgamation of transition sequences in a Markov chain leads to diminishing the number of its states but the statistical characteristic of the resulting transition distribution is no longer memoryless. We will discuss which features of the original process we may still preserve and which ones can bound when investigating the reduced Markov chain.
12 September Ian Stark <stark@dcs.ed.ac.uk>

Seven Trees in One
In the absence of any other speaker, I will be happy to give a brief talk on "Seven Trees in One" by Andreas Blass, which explains why seven binary trees are the same as one, and what this has to do with the square root of -3.
5 September Julian Bradfield <jcb@dcs.ed.ac.uk>

CSL 2000
I will speak about CSL 2000, the Annual Conference of the European Association for Computer Science Logic which took place in Fischbachau/Munich, Germany, two weeks ago.
29 August Rene Vestergaard <jrvest@dcs.ed.ac.uk>

Preservation of Equational Properties
We will present a few readily accessible results about the preservation of confluence, etc., under epimorphisms in Abstract Rewrite Systems. In contrast to the large amount of literature on preservation results for normalisation, it seems that the extant literature on preservation of confluence is restricted to one false claim in a tech report (and its possible reincarnations in later publications). We'll be asking whether this really can be the case.
22 August Conor McBride <ctm@dcs.ed.ac.uk>

Linear Contexts in Regular Datatypes
Regular datatypes (core ML's equality types, more or less) are inductive types generated by polynomial type functors closed under least fixed points. As such, the data they contain are tree-like. Given any such type, a useful auxiliary structure is the associated notion of `linear context' or `tree with one subtree deleted' or `tree with a hole' or whatever you want to call it. These record not only the path we take from root to hole (or vice versa), but also all the subtrees we pass by on the way, so that we have the entire context surrounding the hole. One sunny afternoon, I was waiting for a connection at Shrewsbury and wondering how to construct the type of linear contexts for an arbitrary regular datatype. I was suddenly overwhelmed by a sense of deja-vu...
8 August Francis Tang <fhlt@dcs.ed.ac.uk>

Aspects of flying a glider
Most people think of commercial jet planes when they think of flight: flight as a means of transport from A to B. Then there are some people who fly for nothing more than recreation. Of these people, there are some, who fly exclusively in unpowered aircraft - gliders.
At first, it appears that an aircraft without propulsion is of little use. However, once they have been lifted into the air by external means, they are surprisingly agile and a delight to fly.
For this lablunch talk, I will give a brief overview of flying a glider: at first, the general principles of flight control; then specifics about gliders.
1 August Tomasz Luczak <tomasz@dcs.ed.ac.uk>

Cells and cellular automata
In the talk we describe a simple model of a random cellular automaton introduced by S.A.Kauffman to study chemical reactions which take place in a living cell. We also comment briefly on its rather surprising behaviour indicated by numerical simulations.
25 July Martin Wehr <wehr@dcs.ed.ac.uk>

A Dream of Unity (a geometrical viewpoint)
I want to present a collection of results and indications which seem to form one big picture. Underlying this movement in mathematics are the emerging notions of higher dimensional algebra (also known as post-modern algebra). The motivation for this development come from mathematical physic (attempting to unify quantum theory and relativity). Surprisingly the same mathematical structures can be found in a far reaching mathematical program known by the name of Langlands.
I will finish my talk by relating higher dimensional notions to models of computation. If guided by the beauty of theory one might expect that higher dimensional notions will lead to a unified calculus of computation overarching functional behaviour, side-effects, syntax-semantics duality and type hierarchies.
18 July Peter Hancock <pgh@dcs.ed.ac.uk>

Some coinductive types are understandable
16 May Jan Jürjens <jan@dcs.ed.ac.uk>

Secure Information Flow
I will give a non-technical overview on some recent work on Secure Information Flow. The aim is to ensure confidentiality in a multi-level security model. Results include compositionality (solving a problem from 1992) and an inductive characterisation. Current work tries to bridge the gap between the formal model and cryptographic treatments, following Abadi and Rogaway (TCS 2000).
Ref.
- "Secure Information Flow for Concurrent Processes", Concur 2000
- "Verification of Secure Information Flow", submitted
- "Secure Information Flow with Encryption", in preparation
9 May Bruce McAdam <bjm@dcs.ed.ac.uk>

Life at Microsoft Research, Cambridge
2 May Stuart Anderson <soa@dcs.ed.ac.uk>

Information power grids, e-science and Computer Science Research
Right now the UK science community is all fired up about developing Information Power Grids to support computationally intensive e-science. They all feel they need to engage with Computer Scientists in order to do this -- but the CS community is thought to be reluctant to get involved. All this is being played out at very high level of science policy maiking in the UK but it may have a strong impact on the future direction of UK Computer Science funding. I'll give an overview of IPGs, likely policy directions, how it might affect us and some of the issues that IPGs raise in Computer Science research.
25 April Stuart Anderson <soa@dcs.ed.ac.uk>

Getting Formal Proof into an Industrial Software Development Process
Most of us think that getting commercial software developers to use formal proof would greatly improve the quality of software. This is less obvious to managers who oversee traditional development methods. I'll describe my experience of one company's approach to adopting a more proof-based approach to software development and some of the issues involved in making such a change.
11 April Rod Burstall <rb@dcs.ed.ac.uk>

IFIP working group 2.3 programming Methodology
I will give an outline of last week's meeting near Newcastle.
4 April Michael Fourman <Michael.Fourman@ed.ac.uk>

Propositional Planning
Ordered Binary Decision Diagrams (OBDDs, Bryant) provide a representation of Boolean functions, which is widely used to verify temporal properties of large finite state systems (eg. Model Checking, Clarke). OBDDs have been found to allow exhaustive state space explorations that are often far more effective than proof searches.
STRIPS is a formalism for describing planning problems. A planning domain is a labelled state transition system, whose states are determined by a finite set of propositional variables, and whose transitions are labelled by "actions" that define the transitions as conditional updates of these state variables. A planning problem is to find a path in this transition system (ie. a sequence of actions) that leads from some initial state to a goal state.
I'll give brief introductions to BDDs and to STRIPS planning. I'll then explain how STRIPS actions can be directly encoded using simple operations on BDDs, rather than using the general representation of transition systems introduced by Clarke and Bryant, and how this representation forms the basis of PropPlan, a novel planning algorithm.
28 March Jenny Flemington <jenny.flemington@ed.ac.uk>

Library services - update, with focus on electronic services
This will be a brief talk on some of the recent changes in Library services, looking in particular at online services. We would like to use this as an opportunity for people in Informatics to raise questions and give feedback on current service provision by the Library.
21 March Martin Lange <martin@dcs.ed.ac.uk>

Several examples that should prevent us from doing a prognosis about something in the future, together with some examples that should encourage us to do so.
"640k should be enough for everyone's purposes." is maybe the most famous but not the only `forecast' that has been proved wrong in the meantime. I shall present a few other examples, together with some that were (surprisingly?) shown to be right. Most of them are related to computer technologies, the others are taken from some other scientific fields. Unfortunately I couldn't find specific computer science forecasts, but everyone is welcome to complete my list with things like:
- "Our grandchildren will have to do the P=PSPACE proof as a homework in primary school mathematics." or
- "By 2037 every house will have its own quantum toaster." etc.
14 March Francis Tang <francis.tang@dcs.ed.ac.uk>

Encoding Abadi and Leino's Logic of Objects (AL) in LEGO (joint work with Martin Hofmann.)
I will give a brief summary of our attempt at encoding a logic of objects in LEGO. To minimise implementation overhead, we use Higher-Order Abstract Syntax. We are working on a soundness proof which is tricky because AL's proof is syntactical.
7 March Rod Burstall <rb@dcs.ed.ac.uk>

ProveEasy: helping people learn to do proofs
I'll talk about the tutorial system for natural deduction proof which I have written, and I will give a demo.
29 February Phil Scott <phil@site.uottawa.ca>

What is Godel's Dialectica Interpretation?
In 1958 Godel published an interesting note in the philosophical journal Dialectica, giving a consistency proof for arithmetic that he had first developed in the early 1940's. This short, deceptively simple, paper has greatly influenced modern constructive mathematics, proof theory, and lambda calculus, and indeed categorical logic. In particular, some of the "classic" papers by Tait, Spector, and Girard, as well as works by Prawitz, Troelstra, and Bishop, come directly from contemplating Godel's Dialectica paper. More recently, it has been used by S. Cook and A. Urquhart for analyzing bounded arithmetical theories. The many footnotes added by Godel have a decidely "modern" flavour, and suggest Godel even had a "game-theoretic" intuition of his work.

In my own case, it was explicitly to understand the underlying principles of the Dialectica Interpretation that Lambek and I wrote our 1986 book on categorical logic. I'll give a brief historical tour of Godel's paper.
22 February Peter Hancock <pgh@dcs.ed.ac.uk>

A hands-in-the-pocket presentation of the Mahlo universe.
A hands-in-the-pocket presentation means one without visual aids, even gesticulation. A universe is a collection of sets (or datatypes) indexed by a set which is closed under one's favourite set-forming operators. A mahlo universe is a universe which contains for anyone's favourite family of set-forming operators a universe closed under the appropriate restriction of those operators.
For your entertainment, I'll try to explain the basic idea of a Mahlo universe, and what interests me about them. I will even do it in handcuffs, if someone brings a pair.
15 February Perdita Stevens < Perdita.Stevens@dcs.ed.ac.uk >

Semantics for UML: what could it and should it mean?
There are moves afoot to formalise the existing informal semantics of the Unified Modelling Language. I'm not directly involved in this but I am an interested bystander, and it seems important that someone solicits input from people who specialise in semantics. I propose to say a very few words about what UML is and what it seems to me one might want to do with a semantics, and hope that the assembled wisdom of the LFCS can say some more about that and about what the implications are for what kind of semantics should be being defined.
8 February Don Sannella < dts@dcs.ed.ac.uk >

Funding from the European Commission for theoretical computer science
A few weeks ago I went to a meeting at the European Commission in Brussels to discuss the European funding situation in theoretical computer science and to brainstorm about topics for possible future funding initiatives. This talk is to report on what happened.
1 February Eric Vigoda < vigoda@dcs.ed.ac.uk >
I'll describe the Markov Chain Monte Carlo method and its relationship with phase transitions in statistical physics.
18 January Julian Bradfield <jcb@dcs.ed.ac.uk>

Making the most of your intellectual property
Last week I attended an EPSRC-organized seminar on "Making the most of your intellectual property". I'll give a brief report on this.
11 January Daniele Turi <dt@dcs.ed.ac.uk>

Noam Chomsky
Over Christmas I have read various challenging books by Noam Chomsky including one exposing the dangers of globalizations. I would like to discuss some of his ideas in our LFCS forum.

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