• People
• Events
• Research

Lab Lunch Talks 1999

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

• 7 December
  
  Ad-hoc talk
• 14 December Jan Jürjens <jan@dcs.ed.ac.uk>
  
  Security and Confer-2

  I will talk about the DERA/RHBNC Workshops on Secure Architectures and Information Flow (last week in London) and the meeting of the Confer-2 working group (the week before in Paris) (http://para.inria.fr/confer/).

• 30 November Bruce McAdam <bjm@dcs.ed.ac.uk>
  
  Informatics at the SCI-FUN Roadshow

  Some Computer Science based activites have recently been added to the SCI-FUN Roadshow (see http://www.ph.ed.ac.uk/scifun/). I will demonstrate the activities and give you an opportunity to comment on them.

• 23 November Robert Tennent <rdt@cs.queensu.ca>
  
  Looking back at Strachey's "Fundamental Concepts"

  The previously unpublished lecture notes from Christopher Strachey's "Fundamental Concepts in Programming Languages" lectures in 1967 are about to be published. In this talk I will look back at the influence that Strachey and his collaborators had on the development of our understanding of state in imperative languages.

• 16 November Daniele Turi <dt@dcs.ed.ac.uk>
  
  Domains in China

  I will report on my recent trip to Shanghai, China, where I have attended an International Symposium on Domain Theory (URL: http://www.cs.uga.edu/~gqz/ISDT.html).

• 9 November Paul Jackson <pbj@dcs.ed.ac.uk> Total correctness of reactive refinement In a previous lab lunch, Samson Abramsky presented a `reactive refinement' relation: if A and B are reactive systems capable of input and output actions, then A c= B (read `B refines A' or `B is an implementation of A') if (roughly speaking) B accepts at least the input actions that A accepts, and if any output action generated by B is also OK by A. The relation has a `safety' flavour about it: if B does some output action, then that's correct by A, but there is no guarantee that B outputs anything at all in situations in which A has the possibility of outputting something. I'll discuss conditioning A and B such that if A c= B is established, B is guaranteed to generate some output whenever A would. This then ought to ensure that A can be replaced by B. I'll tie matters down with an example where the reactive systems are heap memories that might be garbage collected.
• 2 November Dan Ghica <dang@dcs.ed.ac.uk> Baby Semantics for a Fragment of Idealized Algol In the games semantics for second-order Algol terms in beta-normal form and without recursion, complete plays can be described using regular expressions. The semantics is fully abstract and it permits the verification of all typical Meyer-Sieber-like equivalences by a trivial calculus of regular expressions.
• 26 October Richard Mayr <mayrri@dcs.ed.ac.uk> On the Hardness of Bisimulation This talk gives an overview over results about the problem of deciding bisimulation equivalence on several different classes of processes. In some cases bisimilarity is decidable in polynomial time, while in others it is much harder. As a special highlight we describe some new results on lower bounds for bisimulation problems, e.g., 1. Strong bisimilarity of pushdown automata is PSPACE-hard. 2. Strong bisimilarity of Basic Parallel Processes (BPP) is co-NP-hard. 3. Weak bisimilarity of BPP is \Pi_2^p-hard in the polynomial hierarchy.
• 12 October: No talk.
• 19 October Rod Burstall <rb@dcs.ed.ac.uk> Comments on Lab Lunch
• 5 October John Power <ajp@dcs.ed.ac.uk> Models for the computational lambda-calculus I shall present a version of Eugenio Moggi's computational lambda calculus, with an explanation of why I think this formulation is worth consideration. I shall then describe two sound and complete classes of models for it, explain the definitions, and outline why one might be interested in them. The first class is that of closed Freyd-categories, a natural and direct generalisation of the notion of cartesian closed category. The second is that of closed kappa-categories, which are based upon indexed categories and which are related to modern compiling technology.
• 28 September Samson Abramsky <samson@dcs.ed.ac.uk> LFCS Organization and Strategy I would like to raise some ideas and proposals for comment and discussion.
  • 1. The LFCS Directorate The current proposal is to replace the present arrangement, whereby the Professors within LFCS are the Co-Directors, by the following. The Directorate will consist of the Director and Assistant Director, plus four Co-Directors, two of whom are nominated by the Director, and two of whom are elected by the members of the LFCS Research Committee. It is also planned to review the remit of the Research Committee, with a view to enhancing its role.
  • 2. LFCS within the Division of Informatics It might be useful to share information, and gather people's views
  • 3. Future Directions and Research Strategy Should LFCS have a research strategy, and if so what should it be?
• 21 September Jane Hillston <jeh@dcs.ed.ac.uk> Report on the Multi-Workshop on Formal Methods for > Performance Evaluation and Applications
• 14 September Ian Stark <stark@dcs.ed.ac.uk> Report on the 1st Scottish Functional Programming Workshop
• 7 September John Longley <jrl@dcs.ed.ac.uk> Eclipses Alex and I went down to Cornwall for the total eclipse earlier this month. I'd like to share some of the interesting things I've been learning recently about eclipses and how to predict them, in a bit more detail than we got in most of the media coverage. Topics will include hybrid eclipses, saros and inex cycles, the long-term effects of tidal friction and, of course, some future dates for your diary.
• 24 August Ulisses Ferreira <juf@dcs.ed.ac.uk> Global Computation Needs a Global Solution Global Computation (GC) can be seen as an extention of mobile computation on a public wide-area network where the constraining factor is the speed of light. An internet-like environment can primarily be seen as a huge, inneficient and non-trustable computer instead of a network. This leads to a new programming paradigm.
  In this talk, I will discuss problems, and solutions, that arise from Global Computation. Then, I will explain why there is no programming language or system to date that fully permits GC, at least directly. Finally, language concepts and constructs will be introduced to solve these problems.
• 17 August Chris Walton <cdw@dcs.ed.ac.uk> An Abstract Machine for Memory Management In composing the Definition of Standard ML, the authors chose not to give an account of the operation of memory management. This was the right decision when focussing upon the abstract description of a sophisticated high-level language. However, the issues associated with memory management cannot be ignored by the compiler writer who must make decisions which have a great impact on the performance of the compiled code. In my talk, I will present an abstract machine formalism of a tag-free garbage-collector which exposes many important memory management details such at the heaps, stacks, and environments.
• 29 June Daniele Turi <dt@dcs.ed.ac.uk> Abstract Syntax and Variable Binding I shall give a 20 minutes, high-level explanation of the recent work by Marcelo Fiore, Gordon Plotkin and myself on abstract syntax with variable binding, which I am going to present at the LICS conference.
  We associate to every binding signature a category of models consisting of variable sets endowed with both a (binding) algebra and a substitution structure compatible with each other. The syntax generated by the signature is the initial model. This gives a notion of initial algebra semantics encompassing the traditional one: besides compositionality, it automatically verifies the semantic substitution lemma.
• 15 June Peter Hancock <pgh@dcs.ed.ac.uk> Conway Games John Conway is a mathematician with interests in number theory and the theory of games. One of his inventions is "surreal" arithmetic, a heady cocktail of transfinite ordinals, infinitesimals, the continuum, and game theory. Even in a teetotaller, some curiosity is excusable. I'll pass on a few rumours I have heard about his arithmetical ludo.
• 4 May Perdita Stevens <pxs@dcs.ed.ac.uk> SLI: the tale continues I plan to give a report on the Research Workshop of the Institute for System Level Integration, which will have happened the day before, on Monday 3rd May. This looks as though it may be a low-propaganda high-content day, compared to previous events, so I'm hopeful there will be plenty of new things to say arising from it. If not, I'll talk about something else!
• 27 April Samson Abramsky <samson@dcs.ed.ac.uk> On Refining Reactive Systems Refinement of a specification is one of the key notions in formal methods. This notion is usually developed in a ``static'' setting, for programs viewed as functions or relations. The question arises of how best to refine refinement for the purpose of specifying and developing reactive systems. In discussions last year with a group based at AT&T Bell Labs interested e.g. in specifying telephone exchanges, they raised the problem of getting a compositional notion of refinement which took proper account of the System/Environment distinction, which is basic to their work. I realized that I knew of such a notion, which had arisen for other reasons in my work. The slogan: as repeated System/Environment interactions refine sets, so ``reactive refinement'' (or back-and-forth simulation) refines set inclusion.
• 13 April Stephen Eglen Institute for Adaptive and Neural Computation <stephen@anc.ed.ac.uk> Modelling the development of retinal mosaics with simple neural networks Retinal cells are regularly spaced throughout the retina of humans, cats and many other species. This regular tiling ensures that the visual world is processed efficiently and with complete coverage ("no holes in visual space"). The patterns of cells are therefore known as retinal mosaics because of their resemblance to other types of mosaic.
  An important issue in developmental neuroscience is how these mosaics are created from an initial population of randomly-positioned cells. In this talk I will present a neural network model to show how lateral cell movement may account for normal mosaic development. The model can also dynamically adapt to either increases or decreases in network size during development. I will finish the talk by mentioning ongoing work comparing the model with experimental data.
  See http://www.anc.ed.ac.uk/~stephen/mosaics for movies of network development. This work is in collaboration with Arjen van Ooyen (Netherlands Institute for Brain Research).
• 6 April Michael Fourman <mikef@dcs.ed.ac.uk> Universal Information Ecosystems See http://www.cordis.lu/ist/fetuie.htm
  In part this stems from an LFCS proposal for a european programme in Global Computation. However, the scope of the Initiative is *much* broader.
  I quote from the Call:
  "UIE stems from the vision of an emerging information "ecosystem" that constantly scales up or down, evolves and adapts in order to best meet the changing demands of its vast and highly dynamic population of "infohabitants" (for which it is not unreasonable to think of trillions). The benefit would be an environment that supports the dynamic creation of new types of relations and activities and, in doing so, creates value and degrees of scalability, sustainability and robustness that are well beyond what can be envisaged today."
  Don and I attended the launch of the programme in Brussels on 18th March, and various parts of Informatics are involved in discussions that should lead to several proposals going forward.
  I'll report on the Brussels meeting and the current state of play.
• 30 March John Longley <jrl@dcs.ed.ac.uk> A bigger slice of pi": Exact integration is almost feasible! Recently at ML Club I talked about some of my algorithms for doing exact real-number integration. Shortly afterwards, I realized that there were much much more efficient approaches to integration, which I'll talk about here. I haven't implemented them yet, but I think they ought to allow quite a large class of definite integrals to be computed to about 20 decimal digits in reasonable time, in an "exact" setting for real-number computation.
• 23 March Dave Robertson <dr@dai.ed.ac.uk> Restricted Systems of Refinement for Horn-Clause Programs When building a system which synthesises programs by refinement from early descriptions, we must have a language for expressing refinements and a method for choosing the refinements appropriate to the task in hand. It might seem that the best way to do this is by devising a parsimonious, general-purpose refinement language and a flexible way of choosing refinements. Unfortunately, it is difficult to make such systems attractive to use - as I shall explain with an example. One way around this problem is to target a narrower class of tasks and produce for these collection of more detailed refinements tuned to a more focused method of refinement choice. I give an example of this and use it to discuss the tension between focus and generality. The programs produced by both examples are described as Horn Clauses but the problems discussed apply to any formal refinement system.
• 16 March Julian Bradfield <jcb@dcs.ed.ac.uk> Fixpoint alternation, Rabin conditions, and the game quantifier Drawing inspiration from the theory of finite automata on infinite objects, I have a new (as far as I know) refinement of the so-far known characterization of the power of the game quantifier in effective descriptive set theory---aand conversely, the first comprehensible characterization of the levels of the fixpoint alternation hierarchy in arithmetic. In this talk, I'll just explain the result with minimal technicality.
• Martin Hofmann <mxh@dcs.ed.ac.uk> Inherent parallelism in "exact" real number computation In the Scott-Escardo-Edalat-Potts-Jung-... approach to arbitrary precision computation with real numbers the real numbers (in [0,1]) are modelled as the domain of closed subintervals of [0,1] ordered by reverse inclusion.
  A one point interval represents an honest-to-good real number; a proper interval [a,b] represents partial knowledge, i.e. that our number lies within a and b, in particular [0,1] reveals no information so that's "bottom". Martin Escardo has argued convincingly that --- if we aim for Turing completeness --- then we must accept these partial real numbers in just the same way as we have to accept partial functions in a Turing complete programming language for integers.
  In Martin's toy programming language "Real PCF" there is a parallel conditional pif defined by pif(true,x,y)=x, pif(false,x,y)=y, pif(bottom,x,y)=greatest-lower-bound(x,y). Notice that the g.l.b. of two intervals is the least interval containing their union.
  Although we don't have formal evidence we feel that such parallel construct must necessarily lead to inefficiency because when computing pif(b,x,y) as long as we don't know what b is going to be we must evaluate both x and y in parallel. If the pif occurs in the body of a recursive definition (as it usually does) then it seems that we double the number of active processes each time we unfold the recursion!
  Therefore, it may seem natural to ask whether there might be a version of "Real PCF" which does without the pif or similar parallel features.
  The main research goal formulated in the visiting fellowship grant application for Thomas Streicher was to prove that parallelism cannot be avoided if one adheres to the interval model.

  After becoming increasingly desperate we finally managed to prove this about three days before Thomas left. Our result is as follows:
  "Let L be Real PCF without pif but with a builtin primitive function f:[0,1]x[0,1] -> [0,1] such that, semantically, f agrees with the binary average function on total numbers (on partial numbers it can do what it wants as long as its Scott-continuous). Then parallel-or on the unit type (por(_|_,_|_)=_|_, por(x,y)=T, otherwise) is definable in L."
  In the talk I'll mainly try to further motivate this and perhaps give an idea of the proof for a simple case.

• 9 March Alan Bundy <bundy@dai.ed.ac.uk> Theoretical Limits on Inductive Proof It is well known that work in mathematical logic in the early part of this century provided a number of negative theorems putting limits on formal representation and reasoning. Best known are Goedel's incompleteness theorems and Turing's proof of the undecidability of the halting problem. It is less well known that most of these limitations apply specifically to inductive reasoning. Nor are they only of purely theoretical interest; they place practical restrictions on our ability to automate inductive inference. I will discuss the practical impact of these negative theorems.
• 2 March Patricia Machado <pdlm@dcs.ed.ac.uk>
  Jo Hannay <joh@dcs.ed.ac.uk>
  Patricia and Jo will report on AMAST'98 (Algebraic Methodology and Software Technology), Amazonia, Brasil, and show some pictures and maybe some video footage.
• 23 February Massimo Felici <mas@dcs.ed.ac.uk> Understanding Requirements Evolution: An Avionics Case Study One of the most important phases of the software life cycle is the specification of requirements. Errors can be recovered effectively during early phases of a project. The complexity of fixing errors increases with the progress of the project and the recovery activity becomes less cost effective.
  Despite the crucial role of specifying requirements there has been slow progress in improving requirements specification and generally in requirements engineering. Recent research has identified some interesting aspects of requirements. Requirements changes are due to several environmental aspects, human factors (e.g., user involvements, stakeholders communications, human skills and knowledges, human behaviours, etc.) as well as domain constraints and aspects (e.g., standards, development processes, internal organisations, product lines, technologies, business targets, etc.). Formal methods are used for specifying requirements as well as for verifying requirements properties. In order to support development activities and the different environmental aspects, the use of formal methods should be more integrated into the development process in the early phases of a project, this is also useful to accommodate changes. The support of formal methods is widely accepted in safety-critical systems, where there are stringent requirements, and in industrial applications. The state of the art in requirements engineering and the use of formal methods, in particular for safety-critical systems and in general for industrial applications, is not yet mature. This is also due to the fact that
  • formal methods only capture some of the requirements
  • it is impossible to capture the requirements at the first attempt in new complex systems
  • requirements must change.
  Moreover, the use of formal methods is affected by Requirements Evolution.
  Most work in requirements engineering tries to specify requirements better. Despite the widely accepted evolutionary behaviour little effort has been spent in order to understand not only requirements specifications but also their evolution. Formalisation may help in the study of requirements evolution and it may be possible to devise specification techniques that admit changes. A deeper understanding of the evolutionary aspects is needed. Further research in requirements engineering should
  • study how requirements change
  • construct requirements specifications expecting changes.
  I will show an investigation methodology to acquire a deeper knowledge of the requirements evolution. The investigation methodology consists of three main steps, namely, Requirements Evolution Characterisation}, Requirements Evolution vs Test Data} and Supporting Requirements Evolution}. Firstly, the investigation methodology aims to define a qualitative description of the requirements evolutionary aspects in terms of type of changes and cause-effect of changes. Moreover, it identifies the variable and non- variable parts of the requirements. The extent to which requirements changes affect the final product is the target of the second step. It aims to investigate relations between requirements evolution and software failures. The final step defines an organisation for requirements specifications expecting changes. In this organisation the software life cycle is part of the requirements; moreover, non-variable requirements are related to architectures and variable requirements are related to components. We started to apply the investigation methodology on an avionics case study. I will introduce some general aspects related to requirements changes of the case study.
• 16 February Jim Laird <jdl@dcs.ed.ac.uk> Computing without data The idea that values can be represented intensionally using functionals has a long pedigree. I'll describe such a representation, and how it can be structured as an invertible cps translation from functional languages with a richer type structure and first-class control. This will be the basis for a look at the denotational semantics of this `intensional functional language' (aka the simply typed lambda calculus), and in particular the problem of describing a fully abstract model. There are connections with sequential algorithms, games, and decidability problems in various lambda calculi. And an interesting contrast with the semantics of traditional functional languages.
• 9 February Carsten Furhmann <car@dcs.ed.ac.uk> Direct models for the computational lambda-calculus Eugenio Moggi's computational lambda-calculus aims to prove operational equivalence for a large class of call-by-value programming languages. The usual models are monads with extra structure, and types and programs denote objects and morphisms, respectively, of the Kleisli category, which we must construct. By contrast, we don't need a construction if we model call-by-name languages by cartesian-closed categories. I shall show how to avoid the Kleisli construction by identifying the necessary structure on the Kleisli category. This leads to direct models which are to call-by-value what cartesian-closed categories are to call-by-name. I shall give the - mathematically interesting - reason why our direct models do the same job as monads. If time permits, I shall use direct models to prove that the computational lambda-calculus has two redundant term formation rules, and to describe and relate what I call thunkable programs and central programs.
  The direct models combine several ideas that evolved over many years in our Laboratory, and I'll tell some of that story.
• 19 January Alan Smaill <smaill@dcs.ed.ac.uk>
• 12 January Richard Mayr <mayrri@dcs.ed.ac.uk> Infinite-State Systems This talk gives an overview over several classes of infinite-state systems which are used as abstract models for concurrent programs (e.g. Petri nets, pushdown processes, PA-processes, ...). Although they are not Turing-powerful themselves, they can still model important aspects of the behavior of `real' programs. These abstract models are easier to analyze and can thus be used for verification.
  We describe a unified representation of infinite-state systems in the framework of term rewriting. Then we give an overview over the decidability and complexity of some verification problems:
  1. Model checking with various temporal logics.
  2. Checking semantic equivalences (like bisimulation).

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