• People
• Events
• Research

Lab Lunch Talks 1995

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

• Dec 12 Yoram Hirshfeld

  Milner's star height conjecture

  By a famous exercise every regular expression over a single letter is language equivalent to an expression without nesting stars. Is this true also for bisumulation equivalence or is there a proper hierarchy of expressions according to the depth of star nesting.
• Dec 5 Masahito Hasegawa

  Recursion from Cyclic Sharing

  Cyclic sharing is a practical technique for implementing recursive computation efficiently. To capture its semantic nature, I introduce categorical models for a lambda calculus with cyclic sharing, using "notions of computation" by Moggi / Power and Robinson and "traced monoidal categories" by Joyal, Street and Verity. Then I explain that the traditional fixed point semantics are the degenerated instances of this new models; in other words, we get recursion from cyclic sharing "semantically".
• Nov. 28 Pawel Paczkowski (Chalmers University of Technology, Gothenburg, Sweden)

  Verifying CBS Processes Using Symbolic Bisimulation

  Symbolic semantics of processes and symbolic bisimulations introduced by Hennessy and Lin have been successfully used as a technical tool in theoretical study of value-passing process calculi CCS and CBS. However, relatively little experience has been gathered so far in using the symbolic bisimulation to verify process correctness. One could expect that symbolic bisimulation would facilitate establishing equivalences between infinite-state-space value-passing processes. In this talk we demonstrate some problems in exploiting the symbolic bisimulations to carry out correctness proofs for CBS processes, and consider some ways of handling these problems.
• Nov. 21 Healfdene Goguen

  Inductive Function Spaces

  Functions in type theory are usually represented using lambda abstraction. We consider instead defining the type A -> B as the type inductively constructed from a name for the elimination principle of A. Application and abstraction are then definitional extensions.
• Nov. 14 Marcelo Fiore

  Syntactic Aspects of Recursive Types

  There are two possible ways of adding recursive types Mu X. F[X] to a programming language or formal system:

  One way, in accordance with the propositions-as-types paradigm, is to introduce term operators

            fold: F[ Mu X. F[X] ] ---> Mu X. F[X]
  

  and

            unfold: Mu X. F[X] ---> F[ Mu X. F[X] ]
  

  for explicitly folding and unfolding an element of a recursive type in order to operate with it.

  Another way, is to keep the term language unchanged and introduce type-equality judgements containing the axiom

            (fold/unfold)   Mu X. F[X] = F[ Mu X. F[X] ]
  

  together with a retyping rule

                             t:A   A=B
  
            (subsumption)   -----------
  
                                t:B
  

  In this talk I will present joint work with Martin Abadi exploring the equivalence of the above two systems via the study of syntactic isomorphisms between recursive types. Applications to information retrieval are envisaged, and will be mentioned briefly.
• Nov. 7 Perdita Stevens

  Integral forms for Weyl modules of GL(2,Q)

  I will attempt to give a brief overview of my ancient thesis, whose title was "Integral forms for Weyl modules of GL(2,Q)". I'll spend a very short time on the algebraic technicalities needed to explain the problem (and the title), but mostly I'll be talking about integers and lattices: there will be pictures.

  Hayo Thielecke

  About the workshop Higher Order Operational Techniques in Semantics

• Oct. 31 Kyriakos Kalorkoti

  Logic, Counting and Algebra

  We show how a well known empirical observation on the runtime effect of the type of order used for Grobner basis computations can be related to a widely held belief in Complexity using examples from Logic (without quantifiers!).
• Oct. 24 Andrew Wilson

  A Hoare Logic for CSP

  I'm going to talk about program verification for parallel programs written in CSP. After introducing Hoare Logics for sequential languages, I'll talk in depth about Apt, Francez and de Roever's Hoare Logic for CSP, giving an example program verification. Time permitting I'll then briefly sketch the proof system of Misra and Chandy, and possibly even my own experimental approach.
• Oct. 10 Ewen Denney

  A Logic for Refinement

  I'll talk about the logic I'm working on as part of my thesis proposal. It's a formulation of first-order intuitionistic logic based on properties, and seems better suited for studying refinement, ie. the stepwise transformation of specifications into programs. It's not too deep, probably not very original, and there's still some problems with my system.
• Oct. 3 Chris Owens

  Isabelle Users Workshop

  Isabelle is a generic theorem prover written by Larry Paulson at Cambridge. A fair sized chunk of the Isabelle community attended the recent Isabelle Users Workshop (although there weren't any of our Antipodean pals there). The talks were the standard range: from brilliant (mine) to incomprehensible, wrong or boring. So I'll tell you about some of the interesting ones, plus the future of Isabelle. One tip: never go for lunch at Clare College.
• Sept. 26 Benoit Caillaud

  Regions & Nets

  In 1990, Erhenfeucht and Rozenberg have shown that the graph-theoretic concept of regions plays a central role in the synthesis problem for Petri-nets. This result has been ever-since extended to different classes of nets: elementary, bounded and typed nets. More interestingly, it yields polynomial algorithms in some cases. In this talk, I will present an overview of this mass of recent results, and show how they are related to parallelization problems.
• Sept. 19 No Speaker
• Sept. 12 Stefan Kahrs

  Polymorphic Recursion and Semi-Unification

  Polymorphism and recursion don't go very well together. It is known since 1990 that type inference in the presence of polymorphic recursion is in general undecidable; the algorithm (even the type system) employed by SML does not always find the most general type. I'll give a few examples showing some useful and some genuinely weird aspects of polymorphic recursion. I'll also explain how type inference for polymorphic recursion is related to the semi-unification problem and what the mysterious "extended occur-check" is all about. Disclaimer: all/most of this is well-known, but perhaps not to everyone in the lab.
• Sept. 5 Julian Bradfield

  Linear time model-checking

  I shall talk (briefly, I hope) about some ongoing work with Javier Esparza and Angelika Mader (of the Technical University of Munich). A few years ago, Colin Stirling and David Walker produced a tableau system for model-checking the linear time mu-calculus on finite systems. The success conditions were rather difficult, requiring reasoning about (in principle) an infinite number of paths through the system. We are aiming to give a tableau system with easier success conditions, and also to generalize to infinite state-spaces.
• Aug. 29 Andrew Barber

  SCILL- Syntactic Control of Interference and Linear Logic, a workshop

  I'll tell you a little bit about Syntactic Control of Interference, and a little bit about Linear Logic, and then I'll tell you about this workshop which I attended in Glasgow at the beginning of the month.

  Claudio Russo

  Report on the ADVANCES IN TYPE SYSTEMS FOR COMPUTING conference

• 22 August 1995 David Aspinall

  Two shows for the price of one!

  I'll give a trip report on the INTERFACES FOR THEOREM PROVERS workshop held in Glasgow last month, and I'll also give an overview of some joint work I've been doing with Adriana Compagnoni on SUBTYPING DEPENDENT TYPES. We have proved the decidability of type-checking for a natural subtyping extension of the LF type system.

• 15 August 1995 Stuart Anderson

  Reliable Software?

  Assessing the reliability of computer systems is dominated by approaches based on measurement but we cannot use measurement to establish the very high reliabilities required in some systems. I'll review the arguments against such systems and ask whether the kind of thing we do in the lab can contribute to analysing the reliability of systems.

• 8 August 1995 Kyriakos Kalorkoti

  A sideways look at resolution

• 1 August 1995 George Cleland

  Diffusion and Innovation Processes: Mechanisms which turn basic science into wealth creating technologies.

  Over the past year we have been studying formal methods research and practice. Part of this study has examined how ideas from basic science progress through stages of application and experimentation, eventually ending up in new engineering processes which in turn create jobs and wealth. Traditional diffusion and innovation models are linear in nature. We propose an alternative model which "short circuits" basic research and engineering, thus creating a pool of "applied science" which we maintain is essential for engineering process innovation.

• 25 July 1995 Kevin Mitchell

  Constructor Types in SML

  Constructors are treated as second class citizens in SML. They are the Cinderellas of the SML world; as soon as you pass them around they turn into boring functions. We propose a simple extension to the language that would greatly improve their quality of life. Along the way we also make some observations about subtyping and implicit coercions.

• 18 July 1995 Pietro Cenciarelli

  An ML program that fails to terminate for the weirdest possible reason

  Can you write a nonterminating ML program just using exceptions? That is: no recursive functions, no recursive types allowed... nothing, just simply typed lambda calculus + raise and handle. HINT: it looks like (lambda x.xx)(lambda x.xx) but it is well typed! I was working out the sematics of this fragment of ML and I always required a bottom element in my domains. But then why, if no program could ever loop? Or so I thought. Oh well... the moral is that denotational semantics may give you insights which are sometimes obscure from an operational point of view. If there is time, I will also sketch a proof of adequacy using logical relations involving computational types (monads).

• 11 July 1995 Judith Underwood

  Type theoretic and algbraic approaches to equivalence

  Both type theory and algebraic specification have a number of ways of describing equivalence. In type theory, these include various notions of equality on computations: intensional equality, extensional equality, Leibniz equality, etc. In an algebraic approach, several equivalence relations have been proposed to describe particular aspects of classes of models: behavioural equivalence, abstract equivalence, etc. In this talk, we shall compare equivalence and equality in the two settings, and show how results in one domain can sometimes be interpreted in the other. This correspondence will be demonstrated with a concrete example.

• 4 July 1995 Alan Smaill

  Symmetry arguments in automated problem solving

  It's quite common in mathematical texts to see appeals such as "by symmetry, it's enough to consider ...". It's quite hard to capture such patterns of argument so that they can be used within automated proof systems. One way of doing this is by looking at operations on the syntax of problem representations that leave invariant the properties needed for problem solution. I'll look at some examples, and pictures of jellyfish.

• 27 June 1995 Claudio Calvelli

  Synchronisation in concurrent object-oriented languages

  I'll talk about my recent investigation on the issues related to synchronisation and object-oriented constructs, in particular inheritance. There are many proposals around which aim to solve the interference between concurrency and inheritance. These range from adding language constructs which don't really solve the problems to removing inheritance of synchronisation code completely. My view is that you can divide the synchronisation code in different bits to deal with different issues, and use the most appropriate means to deal with each. In particular, I divide the synchronisation code in two parts - decide whether I can call a certain method, and, if I can, decide which of the waiting caller can proceed. This division allows me to leave the first part to a pure process algebra, with the obvious benefits in terms of reasoning about the system, while the second can be a normal language construct which is only invoked to decide non-deterministic choices. I'll truncate the above to twenty minutes unless the audience shows interest in the subject.

• 20 June 1995 No Speaker

• 13 June 1995 James McKinna

  Report on the BRA Types workshop in Turin

• 6 June 1995 Don Sannella

  TAPSOFT and FMTA

• 30 May 1995 Dave Matthews

  Poly/ML and LEMMA

  LEMMA, a distributed memory system for ML-like languages, has now reached the stage where it will support concurrent progamming in Poly/ML and LCS. In this talk I will describe the programming model for running concurrent applications on a distributed network of workstations in Poly/ML/Lemma and some early results.

• 23 May 1995 Victoria Day

• 16 May 1995 Marcelo Fiore

  Fun: ADT ---> SDG

  After briefly showing you the route that took me from axiomatic domain theory (ADT) to synthetic differential geometry (SDG) I will introduce the first axiom of SDG, prove the basic properties of derivatives, and explain why calculus is not taught this way although it could (should?) be.

• 9 May 1995 Mark Jerrum

  Coupling renaissance

• 2 May 1995 Mike Fourman will re-present the (revised) proposal for an Informatics Graduate School

• 25 April 1995 Claudio Russo

  Decoupling Recursive Types and Variant Types in ML-like Languages

  In most ML-like languages, the value constructors arising from a datatype declaration are directly associated with the defined type. This means that we can't use the same constructor in two different datatypes. Semantically, constructors are just labels. Separating the steps of labelling an expression and injecting the labelled expression into a set of disjointly labelled values makes it possible to re-use constructors and paves the way for a limited, but useful form of subtyping. I'll give a simple static and operational semantics, show how to deal with type recursion, and mention a motivating example.

• 18 April 1995 Stefan Kahrs

  Rewriting Techniques and Applications '95

  I'll be talking about the recent RTA'95 conference in Kaiserslautern, Germany. I shall pick some of the presented papers (and invited talks) of RTA'95 and try to explain in a nutshell what they are all about.

• 11 April 1995 --- no scheduled talk; TLCA conference

• 4 April 1995 Pietro Cenciarelli

  Some thoughts on the notion of evaluation

  If A is a domain for interpreting values and TA one for interpreting programs of type A, how can we define a predicate "P=>v" on (TA X A) that says "program P evaluates to v"? Mind you, the conclusion of the talk will be "boh?", which is the Italian way of saying "I don't know!" Anyway, the idea I will explore is that the type constructor T can be viewed as an algebraic theory and the elements of TA as terms in the language of T freely generated by the "constants" in A. Then, P=>v reads "v occurs in P". Sometimes (e.g. when T is a finitary monad on Sets) this yields the right evaluation predicate. Does it work more generally?

• 28 March 1995 Alan Paxton

  I went to a careers for PhD students thing last week, which was much better than I expected, and what I got out of it may be relevant to others.

• 21 March 1995 Vashti Galpin

  Women in Computer Science

  Recently, concern has been expressed about the low number of women completing Computer Science degrees. I will give some possible explanations for why this happens and some possible solutions to this problem. I will focus on what happens in the United Kingdom, although I will also briefly discuss what occurs in some other countries.
• 14 March 1995 Roope Kaivola

  Axiomatising the Linear Time Mu Calculus.

  The linear time mu-calculus $\nu TL$ is a language obtained by extending standard linear time temporal logic with fixpoint operators. Although the language is known to be decidable, the problem of providing a complete natural axiomatisation for it has been open for some while. In my recent work it has turned out that there is a rather elegant completeness proof for an axiomatisation, based on a new easily negatable normal form for $\nu TL$-formulae. In my talk I'm going to outline the core ingredients of this way to completeness.
• 7 March 1995 Andrew Wilson

  An idea for a concurrent programming language based upon the notion of objectifying interaction.

  Most concurrent programming languages consider interaction to be an event between two processes. What happens if one treats an interaction as a linguistic object? Instead of having separate input and output commands, the idea would be to have one combined "output-and-input" command (eg k:x->y) which would send a k signal from process x to process y. One obvious advantage of doing things this way is the guaranteed deadlock-freeness of one's programs. One obvious disadvantage is that implementation is hard. I'll sketch some ideas for such a language (they're only ideas, mind) --- come along and tell me what you think.
• 28 February 1995 Stephen Gilmore

  Using Type Information to Debug Programs

  Type checking helps programmers to detect errors in programs which are written in strongly typed languages. In a polymorphic language, the benefits of type checking are even somewhat enhanced if types are inferred by the system on behalf on the programmer. In this talk we will consider a simple modification to the usual Damas-Milner type inference algorithm for Standard ML which could be used to highlight certain kinds of errors in programs.
• 28 February 1995 Christoph Lüth

  talks about the recent COMPASS General Meeting in Sintra

• 21 February 1995 Perdita Stevens

  A Shameless Advertisement for the Edinburgh Concurrency Workbench

  I'll talk briefly about what's been happening to the CWB lately, and I'll say a few words about where it's going from here, why, and what the outstanding problems are. Then I'll ask for suggestions from the audience about what you'd like to see it do. The wackier the better (the suggestions, that is.)

• 14 February 1995 Glenn Bruns

  Easy Verification by Program Transformation

  Formally verifying that a program satisfies a property can be tedious because many details -- even some that seem irrelevant to the property -- must be attended to. I'll show how some properties of a simple algorithm can be easily proved by first "erasing" irrelevant details.
• 14 February 1995 Thomas Schreiber

  Formalising Garbage Collection in Type Theory

  Rod Burstall and Adriana Compagnoni have been investigating Garbage Collection in a Unifying Theory of dependent Types. Recently, Adriana and I have represented a fragment of Ben-Ari's imperative garbage collection algorithm in the LEGO system and, resorting to Hoare Logic, proved a modest correctness property.
• 7 February 1995 John Power

  Towards incorporating concurrency into semantics

  A few years ago, Robin Milner introduced control structures in an attempt to model concurrency, in particular the pi-calculus. In doing so, he deliberately avoided traditional denotational semantics in order to be pure to concurrency. His definition was cleaned up with Alex Mifsud's and my help, with no change to the models. Meanwhile, completely independently, Edmund Robinson and I developed a general approach to modelling "notions of computation", reformulating and extending Eugenio Moggi's work. But now, to our great surprise, one can characterize Robin's control structures in Edmund's and my terms. This does not account for dynamics yet, as the dynamics of control structures have not yet been investigated; but it seems an amazing and very promising coincidence.
• 31 January 1995 Chris Owens

  Turning Algebraic Specifications into Model-Theoretic Specifications

  Data-refinement is a well-understood technique (for example, see Jones's book on VDM). How can it be adapted to Standard ML? For a start, one needs to understand how to give specifications which fit in with this style. But this can be hard---ML is not as rich a language as, say, VDM-SL. Algebraic specification is well-suited to ML programs (for example, see any paper on Extended ML).

  In this talk I shall briefly characterise some of the differences between algebraic and model-theoretic specifications. I will then show how to turn an algebraic specification of a Standard ML program into a "model-theoretic" specification, and will discuss how to prove some desirable properties of the "model-theoretic" specification.

• 24 January 1995 Alex Simpson

  An open problem about closed discs.

• 24 January 1995 James McKinna

  will give a short trip report on the recent CLICS/TYPES joint workshop held in Goteborg.

• 17 January 1995 James McKinna

  A modest proposal for (implementing) book equalities

  I would like to talk about some ideas I had at a (very!) recent meeting in Goteborg for implementing book equality reasoning in the LEGO system, based on work in Anthony Bailey's MSc project. This is also somehow an attempt to give a practical understanding of Martin Hofmann's recent work on the elimination of extensionality in type theory.
• 10 January 1995 George Cleland

  A grand day out

  A further demonstration of the audiovisual equipment in JCMB.
• >3 January 1995 -- no scheduled talk, Xmas --

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