- 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:
- Model checking with various temporal logics.
- Checking semantic equivalences (like bisimulation).