• People
• Events
• Research

Lab Lunch Talks 1996

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

10 December	Paul Anderson.		<paul@dcs.ed.ac.uk>
	The Future of LFCS Computing Facilities.
	We want to hold a discussion to try and find out what facilities would be genuinely useful to LFCS research, beyond the desktop workstations that are part of the current standard provision. This includes upgrades of existing hardware (do we need a new/bigger compute server?) and software, but especially new technologies - videoconferencing? Better communications for home working? etc.
3 December	Peter Hancock		<pgh@dcs.ed.ac.uk>
	The paths of righteousness
	A quite natural formulation of the notion of state machine using dependent types is: State : Set Input : ( s : State ) -> Set Output : ( s : State, i : Input s ) -> Set next : ( s : State, i : Input s, o : Output s i ) -> State These structures are very pervasive. They are the structures which parameterise Petersson and Synek's constructor for families of well founded trees, beloved of type-theory buffs. A slight tweak (`monad-isation') of their construction leads to 2 notions of "leafy" or partial tree. These serve as partial descriptions of a state-machine evolving in interaction with an environment, and tie in to game theory, and topology. The talk will be a short enthusiastic rant about them.
26 November	Mark Jerrum		<mrj@dcs.ed.ac.uk>
	Coping with negativity.
	There's a lot of it about. Computational Complexity is far from being immune: for every positive result there seem to be half-a-dozen negative ones. The way to cope with this imbalance is to widen the notion of feasible computation. Randomised algorithms have proved to be one fruitful direction, and approximation algorithms another. Where do we go from here? Recent progress in a number of very different areas begin to suggest a possible way forward.
19 November		National day of industrial action - no talk.
12 November	Alan Bundy	Mathematical Reasoning Group, Department of Artificial Intelligence	<bundy@aisb.ed.ac.uk>
	Rippling: a heuristic technique for guiding search
	Rippling is a heuristic technique for guiding the search for proofs. It works by reducing the difference between two formulae. We will give several successful examples of rippling in a variety of proofs. We use these examples to argue that rippling is a powerful technique that can significantly reduce search while maintaining a high success rate. Even when it fails, rippling can suggest possible patches to the partial proof.
5 November	Don Sannella		<dts@dcs.ed.ac.uk>
	The next ten years of LFCS.
	The original plans for LFCS were for an initial period of ten years. We should also consider if and how these plans should be adjusted in view of changing circumstances, taking into account experience gained during the past ten years. I will lead a discussion on this topic. The discussion will be based on the following papers, which I will assume that everybody has read: Don Sannella: The next ten years of LFCS Samson Abramsky: Balancing the portfolio Most members of LFCS have been told where to find these online. If you haven't been told and want to know, please e-mail me.
29 October	John Power		<ajp@dcs.ed.ac.uk>
	Sketches for categories with algebraic structure.
22 October	Paul Jackson		<pbj@dcs.ed.ac.uk>
	An introductory example of the use of the PVS theorem prover.
	PVS has recently gained a lot of attention as a powerful yet easy to use system for hardware and software verification. Notable achievements with it include the verification of the AAMP5 microprocessor developed by Rockwell-Collins for use in avionics and of Byzantine agreement algorithms for NASA. In this talk I'll use some recent work I've been doing on verifying garbage collection algorithms with PVS to illustrate PVS's specification language and the style of proof in PVS. PVS uses a classical type theory which includes subtypes, dependent types, record types and ML-like abstract data types. Definitions and theorems are grouped into theories which take both type and value parameters. Proofs are developed interactively by invoking procedures similar to tactics found in other theorem proving systems. The procedures support various kinds of reasoning including rewriting, congruence closure, arithmetic reasoning and heuristic instantiation of quantified formulas.
15 October		"Reading Party" at Wiston Lodge - no talk.
8 October	Randy Pollack		<rap@dcs.ed.ac.uk>
	Theories in Type Theory
	There is much interest in modularity, abstraction and instantiation for formal proof checking. For example, if every monoid has a property, then also every group has that property, and if $G$ is a particular group, $G$ has the property. Further, in analogy with programming language modularity mechanisms, we want to allow names to be local, so as to reuse names in different abstractions. It has been thought that sigma types are the basis for implementing modularity and abstraction in Type Theory. It is clear that sigma types represent \emph{structure} (e.g. the type of monoids, the type of groups), but not clear what the relationship between structure and modularity should be. I present work in progress, following a suggestion of Thierry Coquand, where a notion of \emph{theory} as a first class packaging of contexts is used for modularity. The question of whether structures are packaged as sigma types or left unpackaged as telescopes is orthogonal to this notion of theory. This notion is presented as an extension of Type Theory, and is implemented in this way in the current alpha release of LEGO. There are still some problems with the presentation.
1 October	James McKinna		<jhm@dcs.ed.ac.uk>
	International School on Type Theory and Term Rewriting
	James gave us an entertaining account of the recent International School on Type Theory and Term Rewriting at the Glasgow University Department of Computing Science.
24 September	Mike Fourman		<mikef@dcs.ed.ac.uk>
	The Informatics Revue.
	Mike told us all about the Informatics Planning Unit and we discussed the forthcoming "Informatics Review". The "10-year lookahead" document referred to is an important part of this process.
17 September	Stephen Gilmore		<stg@dcs.ed.ac.uk>;
	LFCS Consequences
	`Consequences' is a children's game where a sequence of innocent events leads to a shattering and dramatic outcome, or something. I would like us to play a variant of this game which centres on how the LFCS has, in its simple way, made an impact on general computer science. This game has a serious intention: to solicit input, in a democratic fashion, on all aspects of the LFCS which can be used in publicity material for the LFCS 10th Birthday Celebrations.
10 September	A small group of people gathered over coffee, tea, and biscuits and discussed (among other things) why it should be so difficult to find speakers prepared to give Lab Lunch talks at the moment.
27 August	Stefan Kahrs		<smk@dcs.ed.ac.uk>
	ESSLLI'96 summer school.
	Stefan will talk about the European Summer School on Logic, Language, and Information which he attended recently.
20 August	Ralph Loader (Merton College, Oxford University)		<loader@maths.ox.ac.uk>
Ralph says:	Finitary PCF is Undecidable.
	"The question as to the decidability of the observational ordering of finitary PCF was raised as it was reasonable to hope that a good solution to the full abstraction problem for PCF would give an effective presentation of a model, so that the ordering for finite parts could be read off. "We show that this is not the case. The observational ordering is undecidable. We use encodings of semi-Thue problems as sets of 32 simultaneous inequations. The main difficulty is that because of the rich term structure of finitary PCF, a series of reductions of complicated terms into simpler ones must be carried out, and the encodings used must be carefully chosen so as to make this possible. "A draft version of a paper is available via my home page."
13 August	Samson Abramsky		<samson@dcs.ed.ac.uk>
	LiCS `96 and DIMACS workshop.
	This week Samson Abramsky will report (very selectively) on LiCS `96, and also the DIMACS workshop on computational complexity and programming languages which he attended.
6 August	Thomas Schreiber		<tms@dcs.ed.ac.uk>
	User Interfaces for Theorem Provers.
	Thomas will give a talk about the recent `UITP 96' workshop at the University of York which several people from LFCS attended. There is a good resource for information on the subject at: "URL:http://www.dcs.glasgow.ac.uk/%7Estuart/ITP/uitp.html" and all of the papers accepted at the workshop are available on-line, along with abstracts and links to other goodies at: "URL:http://dcpu1.cs.york.ac.uk:6666/%7Enam/uitp/proceedings.html" The papers presented at the workshop are all fairly easy reading, as the presentations were quite brief.
30 July	Stephen Gilmore		<stg@dcs.ed.ac.uk>
	From SPA Models to Programs.
	Stochastic process algebras have been used to model systems which are composed of concurrently active components. Examples include flexible manufacturing systems and operating system components. We now consider the use of SPAs to craft specifications of systems which are yet to be constructed. Our interest in this question centres on questions related to the systematic development of programs from SPA specifications which will enable collections of specifications and programs to be compared. This is joint work with Jane Hillston and Robert Holton.
23 July	Kyriakos Kalorkoti		<kk@dcs.ed.ac.uk>
	Finite Model Theory.
	Kyriakos recently attended the Finite Model Theory two day tutorial that took place at Swansea on 7-9 July and will be describing the talks and discussing some of the problems/difficulties of the area.
16 July	Samson Abramsky		<samson@dcs.ed.ac.uk>
	LFCS Research Themes
	In the context of the general discussion about the future of LFCS initiated by Don, I will look at the current LFCS research themes, and open a discussion of them. In particular, I'd like to discuss: are the current themes the best way of structuring the work currently going on in LFCS? are there things we should be doing but aren't?
9 July	Olaf Burkart		<olaf@dcs.ed.ac.uk>
	Model-Checking Infinite-State Systems with Property Transformers
	Model-Checking is a powerful technique for the automatic verification of processes. Whereas model-checking for finite-state systems is nowadays well-established, the theory for infinite systems is a current research topic. In this talk I will present a new technique which uses functions on the domain of formulas, called property transformers, in order to model-check infinite-state systems. This approach can be applied to a variety of process classes like context-free processes, pushdown processes, graph grammar processes, and REC_rat processes.
2 July	Donald Sannella		<dts@dcs.ed.ac.uk>
	The future of LFCS after ten years.
	LFCS is now ten years old. It seems timely to reconsider its mission and activities in response to changes which have taken place during this time, and in the light of experience that we didn't have ten years ago. A discussion took place on this topic at the recent LFCS Advisory Board meeting. I would like to lead a discussion on the same topic at lab lunch. Below are some questions to start the discussion going. I welcome comments (preferably by e-mail) from people who are unable to attend. LFCS research themes [ See the LFCS WWW pages if you don't know what the research themes are.] Are these the right themes? Do we have staff to support this range of activity? How do these themes relate to the rest of the world? Are we missing some important areas? Theory versus practice Where should LFCS position itself? What is the best balance (for us) between pure theory, experimental work, applications? Is it now where it should be? Do we want to influence practice? If so, how much? Or should we concentrate on creating theories that are pleasing in themselves and not worry about their applicability? Technology transfer Should we try technology transfer activities again (e.g. short courses for people from industry) or try to accomplish the same thing another way? Should we let somebody else do technology transfer? Who? Should we be trying much harder to do it ourselves? How? LFCS and the University / Faculty / IPU How should we react to the present difficult financial position? How can we take advantage of the broad spectrum of research in the IPU? LFCS and University teaching Should we put more work into making our ideas and results teachable? Should we push our research into our own curriculum more? How? Funding trends Are there any worrying trends? How do we react to e.g. the EC's tendency to withdraw funding for basic research? Is the heavy reliance on EPSRC and the EC likely to become a problem? Should we seek funding elsewhere? Where? General questions Where should our priorities be? Should we shift use of resources, look for more resource? Where? What is the best size for LFCS? What has LFCS achieved? Where has it failed? What does LFCS want to achieve? How? What does LFCS want to be?

More Past Talks

1996

• June 25 Kyriakos Kalorkoti

  Separating Complexity Classes: a Possible Approach

  Currently we know very little in the way of separating complexity classes; e.g., P versus PSPACE. We discuss the difficulties behind these problems and outline a possible way around them.
• June 18 Gordon Plotkin

  Compositionality and Universal Type Theory

  The principle of compositionality or referential transparency is central to denotational semantics. Taking this seriously requires a theory of language. For example, viewing language as a free multi-sorted algebra enables one to express compositionality homomorphically, as advocated long ago by the ADJ group. It also provides a uniform notion of translation between signatures that allows one to pass from the semantics of one language to that of another. However such a theory of language is inadequate, and for several reasons. We consider two of these: the lack of a treatment of binding operators, and the fact that sorts (= types), can themselves have a complex linguistic structure. Making a (partial) identification of type theories with programming languages, we advocate a programme to find a treatment of type theories analogous to the universal algebraic treatment of algebraic theories. With this, the language used to express (typically) domain-theoretic semantics is itself brought into the picture, and one can see compositional denotational semantics itself as translation, in a uniform sense.
• June 11 Rod Burstall

  Inductively Defined Relations

• Jun 4 Judith Underwood

  From verified classical programs to constructive proofs

  Although the connection between proofs and programs makes constructive type theory attractive for formal program development, some aspects of program verification work just as well in classical logic. I'll talk about some ideas for importing results from a classical specification and proof tool (PVS) into constructive type theory. Joint work with Jim Caldwell, NASA Langely Formal Methods Group.
• May 28 Colin Stirling

  A Chomsky Hierarchy for Bisimulation

  Recently I proved that bisimulation is decidable for normed pushdown processes. I discuss this result and how it fits in with a Chomsky hierarchy of processes.
• May 21 Departamental Holiday
• May 14 Paul Steckler

  An ML-like type system for detecting local references

  Distributed Poly/ML is a variation on Standard ML that allows threads to be distributed across a network. A run-time memory manager maintains the illusion of a single address space. Operations involving references (:=, !) are slowed by the need to maintain coherence. If a reference refers to data on a local machine, faster versions of these operations can be used. We modify the ML type system so that reference types are marked as local or escaping.
• May 7 Alex Simpson

  What is a model of Intuitionistic Set Theory ?

• Apr 30 Kohei Honda

  Processes - An elementary approach

  So far the notion of processes --- as opposed to that of functions --- has been studied mainly in syntactic form. Recent work by several researchers, however, might suggest there are other possibilities. Such endeavour, if successful, would result in a basic mathematical abstraction of interacting agents and theory constructed upon it. We discuss one possible approach towards the problem of finding a semantic notion of processes, as well as recent results gained in its course. Our quest started from a semantic study of SK-like combinators of mobile processes, which were discovered in 1993. A simple algebra is found, just based on two ideas, processes and names, then its hidden structure, called symmetries, is analysed using an elementary group-theoretic apparatus. The analysis now leads to another presentation of the same notion, simpler and more intuitive, which somehow dispenses with names. The presentation results in a concise yet solid set-like theory of processes, which offers a basic material with which one can understand various existing theories of processes on a uniform basis. In the talk, basic ideas will be discussed referring to some application of the theory to practical problems. Comparisons with related works, notably interaction cagegories and action structures, will also be given. Technical details will be left to printed material.
• Apr 23 Thomas Schreiber

  The minimum-sum section problem

  Abstract: Minimum-sum sections are apparently regularily employed by statisticians. I will present the formal development of a linear imperative algorithm following David Gries and compare this with the even more(?) formal development ending up with the same program, but this time under the auspices of the LEGO system.
• Apr 16 No speaker
• Mar 19 Claudio Russo

  Static Analysis for Free?

  Some observations: o Programming languages derived from ML by adding exceptions, state etc tend to ignore these features in their type systems. For instance, taking SML = ML + exceptions + state, SML types tell us nothing about the exception raising behaviour of terms. o For ML, it is well known that the principal type of a term tells us more about the term's behaviour than any of its instances. o Moggi's work on monads provides a useful framework for defining the semantics of programming language P by translation into a simpler meta-language M. Usually M is a variant of the simply typed lambda calculus: every term has a unique type. What happens if, instead, we take ML as or meta-language, []:P -> ML as the translation, and for a given program p in P, typecheck [p]? If P's type system ignores certain computational aspects of p, then the ML-principal type of [p] may reveal more of the behaviour of p than the P-principal type of p. This additional information may be of use to both programmer and optimizing compiler alike. I'll illustrate the idea with the concrete example of ML+exceptions (an implementation is available). WARNING: This is a half-baked idea.
• Apr 2 Luis Dominguez

  Report on the 1st workshop on "Formal Methods for Open Object-based Distributed Systems" (FMOODS'96) held in Paris, 4-6 march 1996

  I'll try to give you the gist of its three 1 hour invited lectures and nine sections of three half an hour talks, highlighting aspects which I found more interesting, namely foundational ones that might also be of interest to the "lab". In a nutshell, lectures were: - Processes, Types and Observations, by B. Pierce - Abstracting Object Interactions: some requirements and challenges for models of concurrency, by Gul Agha - Formalising Composable Software Systems: a research agenda, by Oscar Nierstrasz and the talks were grouped in the following themes: - Types and Behaviour - Formalising Object-Oriented Methods - Case Studies I and II - Actors - Open Distributed Processing I and II - Process and Object Calculi - Specification and Design of Distributed Systems For people possibly less interested in the former, I reserve a few brief curiosities I've experienced in Paris, namely about language 4000 years ago - seen in the "Louvre" museum - and about good value student accomodation/meals.
• Mar 26 John Power

  Coherence for monoidal categories

  Many people seem to believe that the only proofs of coherence for monoidal categories have syntactic, inductive arguments, as for instance in Mac Lane's book, or Kelly's strengthening of it. In fact, that is not the case. Coherence for monoidal categories is an immediate consequence of the Yoneda lemma for bicategories, which in turn is a simple consequence of the definitions of bicategory, homomorphism of bicategories, and the like. I shall outline the proof and related issues.
• Mar 19 Stuart Anderson

  About something

• Mar 12 Philippa Gardner

  The Expressive Power of Higher-order Action Calculi

  Abstract: Milner's action calculi are based on the pi-calculus, and provide a unifying framework for investigating many models of interactive computation. Higher-order action calculi are a natural extension, which is similar to Sangiorgi's extension of the pi-calculus with higher-order features. Hassei has shown that the simplest higher-order action calculus is connected with Moggi's computational lambda-calculus. In this talk, I will provide further justification for the higher-order setting, by showing how action calculi with complex dynamics (that is, complex computation steps) correspond to higher-order action calculi with much simpler dynamics. This result provides a first step towards the investigation of the dynamics of action calculi. Knowledge of action calculi is not assumed.
• Mar 5 Mark Jerrum

  ``A random voyage in theoretical computer science''

  Argument: How the Skipper and his trusty crew left the harbour merrily but were becalmed in a sea of conjectures; and how after months of torment the ship was driven by a propitious spirit to a fertile shore; and how the (by now ancient) mariner is constrained to recount his story to those who cannot chuse but hear.(*) [Joint work with Alistair Sinclair (University of California at Berkeley).] (*) Of course, that's a lie; you can just stay away if you don't want to suffer this hoary old stuff.
• Feb 27 Nikos Mylonakis

  Encoding of proof systems for behavioural specifications in UTT

  I will give a top-down and abstract presentation of my work on behavioural specifications and type theory since the beginning of my visit at LFCS in October 1994. First, I will give an overview of metalanguages and the type theory UTT, second I will talk about sound and complete proof systems for behavioural specifications and finally I will provide a sketch of the encoding (and its proof of adequacy) of such a proof systems in UTT.
• Feb 20 Paul Jackson

  Overview of the Mizar proof checking system

  The Mizar system is designed for checking proofs in classical mathematics. Over the past 5 years, perhaps 60 people have authored roughly 400 `articles' in Mizar. Abstracts of these articles are published in the Journal of Formalized Mathematics. FYI, I've included below the index for the last two volumes of this journal. Mizar has been created by a small group of mathematicians at the University of Warsaw, Poland. Currently it only runs on PCs under DOS. I'll briefly describe the system's architecture and present sample material from articles. I'll try to identify what I see as some of the main features that have lead to its success, and I'll also discuss some of the current challenges it faces.
• Feb 13 Julian Bradfield

  The modal mu-calculus alternation hierarchy is strict

  One of the open questions about the modal mu-calculus has been whether the alternation hierarchy collapses; that is, whether all modal fix-point properties can be expressed with only a few alternations of least and greatest fix-points. For some years I have been trying to solve this problem by transferring results from descriptive set theory, and in November I succeeded in constructing suitable encodings between transition systems and arithmetic, and applying a recent hierarchy theorem (by Robert Lubarsky) in arithmetic with fix-points. I'll talk a little bit about the problem, a bit about the encoding, and perhaps a bit about the arithmetic theorem I'm using, which is a fairly heavy piece of set theory.
• Feb 6 Andrzej Filinkski

  Controlling Effects

  I will give a brief overview of my thesis work on monads and continuations. In particular, I will sketch a result stating that any computational effect definable by a monadic translation (including exceptions, state, nondeterminism, I/O, etc.) can be uniformly simulated by continuation-passing. As a consequence, any such effect can be implemented directly as a definitional extension of a language with state and first-class continuations, such as Scheme or SML/NJ.
• Jan 30 Rod Burstall

  On The Santa Fe Trail

• Jan 23 Stefan Kahrs

  On the completeness of type systems

  Frequently one comes across claims (and less frequently: proofs) that the type system of some programming language guarantees sound evaluation. In logic, soundness has a dual: completeness. For type systems such a thing does not seem to exist. ...and that is what I am trying to change.
• Jan 16 Thorsten Altenkirch

  An Application of Higher Order Abstract Semantics

  I will define a semantic interpretation of an LF style presentation of simply typed lambda calculus (some people call this 'higher order abstract syntax'). I will use this interpretation to give a (simpler ?) version of a 'reduction free' normalisation proof. I am still looking for other applications of HOASem.
• Jan 9 Gordon Plotkin

  Unorderable models of the lambda calculus

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