Lab Lunch Talks 1998

report on TPHOLs '98 conference

TPHOLs = Theorem Proving in Higher-Order Logics. This conference started out as being just for the HOL community, but now embraces many other interactive theorem proving communities, including those for Isabelle, Lego, Coq, Lambda, Clam/Oyster, Nuprl and PVS. To date, always HOL groups have hosted it, but next year a Coq group will be hosting. The scope includes, but is not limited to: - hardware verification and synthesis - verification of security and communications protocols - software refinement, transformation and verification - industrial applications of theorem provers - advances in theorem prover technology - comparisons of various approaches to theorem proving - proof automation and decision procedures - incorporation of theorem provers into larger systems - exploitation of external tools within theorem provers - connecting theorem provers together - user interfaces for theorem provers - development and extension of higher order logics I'll talk about what I think were some highlights of this year's conference.

Diagrammatic Syntax and Dynamic Semantics

I'll present Pilling's notation* for complex dynamic interactions synchronised at a number of temporal levels. In the hope that we may strengthen interactions between LFCS and other parts of Informatics, I will draw out connections with both Perception, Action and Behaviour, and Communication and Collaboration. This talk should provide useful background for the forthcoming Informatics event to be held at 8pm on Thursday, 3rd of December in Teviot Debating Hall. I plan to coordinate a multimodal demonstration of the semantics. Anyone familiar with ether the syntax or semantics (rigid conformance to the RSCDS standards is not required), is invited to contact me asap to assist.

Computational limits to approximate measurement: some first steps.

Perhaps the most significant development in quantitative theoretical computer science in the last decade has been in the introduction of analytical techniques for classifying optimisation problems according their approximability. These techniques are based on deep results in the area of probabilistically checkable proofs (PCPs). The situation with respect to measurement problems (volume, counting, evaluating partition functions, integration) is much less satisfactory. There are no deep results to help us here. Or maybe there are. I'll describe some unsophisticated first steps towards establishing negative results for approximate measurement. I'll probably mention some joint work with Martin Dyer (Leeds) and Alan Frieze (CMU). The talk will be entirely informatics free.

Interactive Construction of Programs

In the last year or so I have been working on problems of learning Horn expressions in first order logic. These learning problems are in fact equivalent to the task of interactive construction of logic programs (from examples and questions about their input-output behaviour). The talk will introduce these problems and ideas in an informal way. I will first present the framework and discuss automatic and interactive program construction. I will then illustrate some of the ideas involved in the construction of logic programs.

Pre-logical relations

Logical relations are structure-preserving relations between models of typed lambda calculus. They have many applications. As structure-preserving relations, logical relations resemble familiar algebraic concepts like homomorphisms and congruence relations but they lack some of the convenient properties of such concepts. In particular, the composition of two logical relations is not in general a logical relation. I will present a weaker notion of logical relation where the lifting of the relation on base types to higher types is replaced by preservation of the S and K combinators. These "pre-logical relations" have some of the features that make logical relations so useful -- in particular, the so-called Basic Lemma holds -- but they have further algebraic properties including composability. I have only begun looking at potential applications of pre-logical relations. For logical relations, the representation independence theorem says "if there is a logical relation on A and B that is the identity on natural numbers then A and B are observationally equivalent". With pre-logical relations the "if" becomes "iff".

Education is an admirable thing,...

"Teaching at Edinburgh" is a one-week course run by the University Centre for Teaching, Learning and Assessment. Participation is a contractual obligation for new teaching staff, and I duly attended last month. At lab lunch I shall say something about what was in the course: it's aims, the approach used, and what I got out of it.

A Workshop and a Counterexample

Since I'm wavering between two talks I'd like to give, I'll do a bit of both. First I'll say a bit about the Domains IV workshop in Germany that I went to recently. I'll also talk about a funny piece of recursion theory (dating from 1958) that I heard about while I was there, and which completely demolished my intuition.

Stochastic Modelling and Verification

I will give an overview of the recently started "Stochastic Modelling and Verification" project which is a collaboration between Birmingham, Edinburgh, Erlangen and Mannheim. I will outline the project's objectives and talk briefly about some of the work presented at the first project workshop which was held in Birmingham at the beginning of this month. Since the project is just starting I will be concentrating on what we hope to achieve, how and why, rather than presenting any results.

Initial and final constraints of functor categories

Representing theories as categories and models as functors has open the way to study a great variety of kinds of axiom that can be used to define the intended classes of models as subcategories of functor categories. There is a rich literature on generalisations of equational theories. We will discuss left and right Kan extensions as tools to constrain functor categories. It turns out that left Kan extensions are related to inductively defined data types and functions, and that right Kan extensions are related to co-inductively defined processes and functions combining processes. Using both left and right Kan extension to constrain functor categories allows to define classes of models that are more general then those resulting from iterations of monads and co-monades.

Report on CONCUR and EXPRESS

In the beginning of September the 9th Conference on Concurrency Theory (CONCUR) was held in Nice. The 5th workshop on Expressiveness in Concurrency (EXPRESS) took place as one of several satellite events.

I have attended CONCUR and EXPRESS and will try to summarize my impressions. The other Edinburgh participants are welcome to contribute their thoughts on these conferences and/or the other satellite workshops.

The CONCUR webpage is: http://www.inria.fr/concur98/

Types of Behaviour

I shall report on a workshop on "Types of Behaviour" I have attended recently. This was not a computer science workshop however, but a discussion on various forms of human social behaviour.

Report from APPSEM

APPSEM (Applications of Semantics) is an ESPRIT working group. This group had its first meeting last week in Pisa, Italy. In the tradition of the Lab-lunch I will talk about sight seeing in this area of Italy. Further I will talk about the wide range of presentations at the meeting :

- from very applied : solution of the year 2000 problem

- to deep theoretical insight : on realizability models for sequentiality

Trip reports: from Brno and Palo Alto

I recently attended MFCS/CSL in Brno, and visited the Kestrel Institute in Palo Alto. I will give my impressions of these visits.

Designing a correct calculator object and analysing the "3n+1" problem

I'll present two examples on reasoning about recursion which obsessed me: the first one solving a problem with a (not so) simple program, and the second following a fake "solution" of mine.

Ben Kleinman's Farewell Talk

Before leaving Edinburgh (on 11 Sept at about 7AM), I thought it might be nice to let people have some idea about what I've been doing for the past two years and what I'll be up to for the next twelve months. This regulation length talk will be an overview of my work, creating a development environment for Extended ML. I'll touch on my use of the EML Kit and PVS, and mention some issues with building on other people's work.

A Gentle Introduction to Source File Control

Whether you develop software, write documents or install software distributions, source control is ubiquitous. I introduce the Revision Control System (RCS), the Concurrent Version System (CVS) and the Emacs interfaces VC and PCL-CVS. Non-standard applications (after all, this is an LFCS talk!) include how to synchronise a notebook or a self-administrated machine with the help of CVS and the secure shell (SSH). Despite the many acronyms in this abstract, the talk will be low on technical details and instead focusses on basic concepts behind source control.

Using Isabelle 98 at Edinburgh

A couple of recent LFCS seminars have described formal verification projects using the theorem prover Isabelle. Locals may not be aware that the latest version of Isabelle is available here, supported by me. I'll give a quick outline of the system, how to use it, and why you might like to use it. See http://www.dcs.ed.ac.uk/~isabelle for resources.

On infinite Transition Graphs

We purpose a survey on increasing families of graphs (the finite graphs, the grammar transition graphs, the pushdown transition graphs, the regular graphs, the recognizable graphs) having a decidable monadic second-order theory, and probably a decidable bisimulation.

Proper Negation in Logic Programming

It is well known that logic programming languages make use of the closed world assumption and negation as failure. However, although these concepts are still important, in terms of programming, sometimes it is not desirable. In this talk, I will present informally a prototype of an alternative logic programming language which emphasizes the need for the 'unknown' value, and will introduce the notion of proper negation, which is the only negation in this language. I expect that logic programming languages with proper negation will be more expressive and more appropriate for knowledge representation and non-monotonic reasoning.

Trip report: Dagstuhl Seminar on "The Semantic Challenge of Object-Oriented Programming".

Trip report: Workshop on Proof Theory and Complexity (PTAC '98) Aarhus.

The Naperian combinators

The combinators that correspond to addition, multiplication, exponentiation and nought in arithmetic of Church numerals are functionally complete, as has often been observed. The entertainment value of this observation has been underexploited. Lambda-abstraction is formally similar to a logarithm operator, and has an amusing arithmetic.

Trip report: ICALP'98 25th International Colloquium on Automata, Languages, and Programming

Trip report: ECOOP'98 European Conference on Object-Oriented Programming.

Dagstuhl seminar on "Programs: Improvements, Complexity, and Meanings"

While I was in Germany to arrange our permanent move to Scotland and to say goodbye to friends and family I attended the above Dagstuhl seminar with a somewhat cryptic title. The aim of the seminar was to bring together researchers from programming (especially functional) and complexity theory to see what they have in common, and in particular to address the problem of measuring the complexity of functional programs. In my opinion the meeting did not quite achieve its goal, nevertheless there were some interesting talks of which I will summarise two. The first talk by Oege de Moor and others described a problem which (under certain assumptions) can be computed in linear time in a lazy functional language (eg Haskell) but has an n log(n) lower bound with respect to eager functional programming languages (eg ML). This came as a surprise to me since for one thing a believed that eager languages are faster than lazy ones and for another because I believed that lazy evaluation could be encoded in terms of eager evaluation. The other talk by Bruce Kapron started from the well-known result that a functional F(f,x) is continuous iff there is a function g such that F(f,x) is computable using g (and of course the input f) as oracle. Bruce aimed at defining a notion of "feasible continuity" such that the above result would hold with "computable" replaced by "computable in polynomial time".

Equations Between Recursive Definitions

Recursive definitions play a ubiquitous role in computer science. For example, they are used to specify: programs, grammars, processes, and datatypes. Each kind of example determines an equational theory in which recursive definitions that give rise to equal (or isomorphic) entities are equated. Remarkably, whatever the entities being defined, the resulting equational theory turns out to be the same.

On the LICS'98 preworkshop RealComp'98

I'll summarize the LICS preworkshop on real number computation. The talks were on practical things such as techniques for avoiding round-off errors, and their efficient hardware implementation (Kulish), and theoretical things such as type theory via PERs on the power set of the natural numbers and via the exact completion of the category of topological spaces (Dana Scott). A talk by Reinhold Heckmann is difficult to classify. According to the practicioners it was rather theoretical, but according to the theoreticians it was rather practical.

A discussion on: LFCS in the Division of Informatics

It has been decided, modulo one or two steps of formal approval, that the Division of Informatics will come into existence in August. The Department of Computer Science will become the "Informatics South" sub-division and LFCS will become a research institute within the Division. Teaching in the division will be organized by the Informatics Teaching Organization. Postgraduate students will be looked after by the Informatics Graduate School and Ph.D. students will be affiliated with research institutes. The subject of Computer Science will be the concern of the School of Computer Science. For more details see

Queueing with service interuptions

Queueing theory is widely used for the performance modelling of systems in computing, communications and manufacturing. There are 2 main reasons for studying queueing models with service interuptions: 1) realism : real systems break down so performance models should reflect this 2) challenge : adding service interuptions to queueing models normally destroys all the nice structures that make them easy to solve, so we have to find something new After brief introduction to the subject area I will talk about a model of a manufacturing production line with server vacations. It is not possible to solve this model exactly, in general, but I will show how a good approximation can be made.

A Data Structure for Interactive Type Debugging

I am working on Interactive Type Debugging for Standard ML. In some ways, this is similar to ideas about type inference explanation by other authors, but will go further: actively aiding the program repair process by suggesting modifications to programs which can remove type errors.

Report from the MFPS (7-9 May 98) in London

In the style of Perdita's report on ETAPS in Libon I will talk about both the journey itself and the scientific event. There will be also some multimedia involved with some guest stars.

Discussion of 5th Automated Reasoning Workshop and the 14th British Colloquium for Theoretical Computer Science

At the end of March / start of April, the 5th UK Automated Reasoning Workshop and the 14th British Colloquium for Theoretical Computer Science were held together at St Andrews.

A lightweight specification language for PEPA

(Joint work with Jane Hillston)

Beating the Bounds of Paradise, part 2

Last time, we went as far as it's reasonably possible to go by starting from the bottom and going up. This time, I'll talk about some of the other ways of trying to define the boundary. I'll definitely talk about indescribable cardinals (which allows me to bring in the alarming notion of transfinitely higher order logic), and measurable cardinals, the most important of all large cardinals. I might also mention partition (Erdos, Ramsey) cardinals and compact cardinals. Measurable cardinals are interesting for a variety of reasons. One reason is that it took twenty-five years to find out that they were actually large. Another is that their existence, or non-existence, has an impact on what look like normal mathematical statements -- specifically, Lebesgue measurability of sets of real numbers. The existence of a measurable cardinal also implies some slightly startling things about sets of integers in the constructible universe. (I'll explain what that is.)

ETAPS'98

I recently attended ETAPS, the European Joint Conference on Theory and Practice of Software, in Lisbon. This included FoSSaCS, FASE, ESOP, CC, TACAS, CMCS, WADT, ACoS and VISUAL. I'll say a bit (probably a fairly small bit) about it. Executive summary: Lisbon is a great place to visit (though vegetarians should take sandwiches) and ETAPS was quite fun, too...

Beating the Bounds of Paradise, Part 1: How far can you go ?

Miles of smiles ?

"I would walk five thousand miles and I would walk ..." That's a bit ridiculous, isn't it? But would you walk a mile? Or bike? Or frisbee throw? Maybe a pub-crawl is more your style. Or writing a mile's worth of theorems (proofs optional) really gets you going. This week's talk will focus on just how far we're willing to go. And what motivates us to such lengths. Does it matter if it's for a good cause, or for laughs, or both? Will we cover more distance if we have to pay to play, or will the cost deter us? And is it possible to convince people to pay to watch us, or will we feel the need to pay them to avert their eyes? All members of LFCS are, as usual, encouraged to attend. The topic is appropriate for all levels and no background knowledge is required. It will particularly appeal to computer scientists, theoreticians, logicians, mathematicians, and friendly people. Of course, all others are welcome. I've learned my lesson and will speak for no more than 10 minutes, with a discussion/question period to follow.

Scary stories of safety-critical software

With increasing use of software-control over safety-critical systems, including most transport areas (air, road, rail, sea), nuclear power station controllers; and the prospect of further use in yet more challenging domains - such as unmanned military aircraft and "Star Wars" orbital nuclear "defence" systems - we are quite right to be concerned over the correctness/reliability/safety/security of such software. We claim, and generally believe, that formal modelling and analysis techniques can assist in ensuring these important properties, so why - especially in safety-critical domains - is there still such resistance to these techniques? Are we, at least in part, to blame - and if so, what can we do about it? (Answers welcomed...)

Design for domain specificity

We outline an approach to the design of domain specific languages which attempts to ease the application of formal methods and facilitate proof. The ideas presented are illustrated on a concurrent, diagrammatic language for programmable controllers.

Bisimulation equivalence is decidable for normed Process Algebra

Yoram Hirshfeld and I believe we have the above result. I'll explain what all the words and phrases in the title mean (with the exception of "is" and "for"). In the remaining time I'll try to indicate some features of the proof. This is pretty recondite stuff, but I'll be skipping all the details.

How Computer Science Can Help Clear Mines

Stephen Salter will explain the problem of anti-personnel mines and discuss the design of the Dervish mine-detonating vehicle with video of it in operation with live mines.
A scheme for controlling the movements of remotely operated vehicles to a precision of a few millimetres from a CAD drawing using a high frequency version of the Decca Navigator system in command mode may allow computer scientists to contribute to the project.
(By the way, professor Stephen Salter and his team developed successful wave power systems in the 70s. But Britain decided to go head along with nuclear power instead, thus defending its position as the most polluting country in Western Europe.)

Kleene's wonderful tree

I will take a short stroll through the arboretum of recursive mathematics and look at some of the curious species that grow there: Kleene trees, Lacombe trees, and Gandy trees. I will mention some surprising consequences of their existence, touching on at least two of the following: real-number computation, toposes, the laws of physics, and ordinals.

An introduction to proof nets

Proof-nets are a canonical representation of proofs in Linear Logic as certain labelled graphs. This representation avoids the redundancy of sequent calculus, in which there are many ways of writing what should the same (cut-free) proof. There is a beautiful geometrical criterion which characterizes proof nets (those graphs which can arise from sequent proofs) among all labelled graphs: for each graph we define a set of ``switchings'', and for each switching an associated sub-graph. The criterion is that for each switching, the associated sub-graph is a tree (i.e. is acyclic and connected).
The aim of this talk is to give a self-contained introduction to proof nets, and to the above characterization theorem. No previous familiarity with Linear Logic or proof nets will be assumed.

THE QUANTUM FUND A Discovery Fund for Academic Innovations

The Quantum Fund Ltd is a venture fund with the view that the academic researcher should be allowed to carry out his/her research unencumbered with the problems that small company growth can bring. The Quantum Fund is specifically geared to funding the very early stage of the research process where concepts need to be proven or bench models designed and built. They have a representative at The Technology Transfer Centre at King's Buildings.

A Bluffer's Guide to Ordinals (Part 2)

What is an ordinal?
What do `regular' and `inaccessible' mean?
What is an ordinal notation system?
How can I use these things in my programs?
When would I want to?

The structure of the categories of simulations, bisimulations, and data refinements

We analyse the structure of the category Sim whose objects are finitely branching L-labelled transition systems for a finite set L, and whose arrows are simulations. This analysis is equivalent, by a much studied category theoretic correspondence, to the study of the locally ordered category Bisim of bisimulations. We give an axiomatic treatment of Sim as the category H-Coalg for an endofunctor H on Set. Under some conditions, H-Coalg is complete, cocomplete, symmetric monoidal closed, and has a subobject classifier. In fact, it is locally presentable as a symmetric monoidal closed category, and hence an appropriate base for enriched categories, i.e., it makes sense to consider Sim-categories. In the case that L = 1, the subobject classifier is the set of hereditarily finite non-well founded sets.
Sim and Bisim are special cases of the two main category theoretic accounts of data refinement: Sim is a special case of Tony Hoare's account based on natural transformations between structure preserving functors from what he calls a language L into Set; and Bisim is a special case of O'Hearn and Tennent's account based on logical relations. One result lifts from H-Coalg to Hoare's formalisation of data refinement. The others cannot hold in such generality, but may still be open to an axiomatic treatment.

A Bluffer's Guide to Ordinals (Part 1)

All theoretical computer scientists are invariably assumed to be intimately acquainted with transfinite ordinals. However, rather few computer scientists, and not all that many mathematicians, ever get taught about them, so it's not uncommon to muddle through for years until the time comes when you actually need them yourself---meanwhile, random people throw them around in talks, and you're never quite sure how much you need to understand. (This process continues indefinitely, since some proof theorists do pretty bizarre things with them, which normal people don't ever learn about.) If this sounds familiar, this talk is for you: I intend to start right at the beginning, and take a more or less guided tour through the landscaped garden part of the world of ordinals---that is, the part below \epsilon_0---with an occasional glance over the fence. I hope to point out some key facts, so that you don't have to read all the boring stuff in the standard texts. What about Part 2? Part 2 should be a safari in the wilder parts of the realm---but there are infinitely more qualified people than myself here, so I hope that peer pressure will encourage that person to do Part 2!

Grand Challenges for LFCS

LFCS has recently been asked to come up with ideas for future major research initiatives ("grand challenges"). The context will be outlined and two possible grant challenges will be presented:
Don Sannella: Global computation
Stuart Anderson: A theory of testing