• People
• Events
• Research

Lab Lunch Talks 2001

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

• 18 December Perdita Stevens <Perdita.Stevens@dcs.ed.ac.uk>

  Determinacy and well-definedness in a specification language

  OCL, the Object Constraint Language, is a specification language which forms part of UML, the Unified Modelling Language. It is intended to be formal and yet accessible to any developer. This is an ambitious aim and at present, it arguably fails on both counts. Efforts are going on to revise the language for UML2.0 and Juliana Kuester Filipe and I attended a workshop about the revision at UML2001. A statement of OCL constrains an implementation of a UML model. That is, the constraint is written in the context of a given UML model, and in principle, given an implementation of that model you can tell whether or not the implementation also satisfies the constraint: the constraint evaluates to a value in the context of an implementation of a model. The trouble is that certain aspects of OCL are left deliberately undefined, with the effect that the same constraint might legitimately be evaluated both to True and to False in the same context. I failed to convince the group revising OCL that this is a Bad Thing, but we did manage to take away the task of suggesting changes to the language so that uses who wish to avoid this "feature" may do so. We (Juliana, Julian Bradfield and I) are in the process of writing the proposal and would like some advice on the choices this involves.

• 11 December Ian Stark <stark@dcs.ed.ac.uk>

  Internet broadcasting: International Review of UK Research in Computer Science

  International Review of UK Research in Computer Science
  -Presentation of Report - Fred Schneider
  -EPSRC Response - John O'Reilly
  1 p.m., Tuesday 11 December
  IEE, Savoy Place, London with simultaneous live broadcast on the Internet
     http://www.iee.org/Events/a11dec01.cfm
  Technology permitting, there will be showings of this in
  - JCMB common room 2510, and
  - 80 South Bridge E20 AKT conference room
  All are invited to come along and watch (space in South Bridge is limited, so please let Austin Tate know if you are interested.)

• 4 December Javier Esparza <jav@dcs.ed.ac.uk>

  Presentation of `International Review of UK research in Computer Science'

  There will be a short presentation and then discussions on the recent report `International Review of UK research in Computer Science' (see http://www.iee.org.uk/Policy/CSreport/).

• 20 November Monika Maidl <monika@dcs.ed.ac.uk>

  Report on Dagstuhl seminar: Exploration of Large State Spaces

• 30 October John Power <ajp@dcs.ed.ac.uk>

  Kleisli categories

  I have been asked to give a brief talk on Kleisli categories. Kleisli categories were introduced in the mid 60's, and the definition and category theoretic results about them are widely available in elementary books on category theory and in a variety of computer science papers. So, rather than bore those people who either know about them or are uninterested in them, I shall try to give a more personal view of Kleisli categories: why people have used them in denotational semantics, and what I think of their efforts.

• 23 October Alin Stefanescu <Alin.Stefanescu@dcs.ed.ac.uk> and Fedor Fomenko <F.Fomenko@sms.ed.ac.uk>

  Report on Marktoberdorf International Summerschool 2001

  The "Marktoberdorf Summer School" is a two weeks course for young computer scientists and mathematicians working in the field of formal systems development. The course aims at the dissemination of advanced scientific knowledge and the promotion of international contacts among scientists. The speakers will share their experiences of this year summerschool and will provide information about next year courses for those students interested in attending them or for those supervisors that may encourage their students to apply. (http://www4.in.tum.de/div/summerschool/).

• 9 October Francis Tang <fhlt@dcs.ed.ac.uk>

  Report on TPHOL 2001

• 2 October Julian Bradfield <jcb@dcs.ed.ac.uk>

  Report on CSL 2001

• 28 August Ian Stark<stark@dcs.ed.ac.uk>

  Report on Concur 2001

• 3 July Martin Lange <martin@dcs.ed.ac.uk>

  Three months at BRICS

• 26 June Masahito Hasegawa <mhas@dcs.ed.ac.uk>

  Report on TLCA 2001

  I shall give a report on the TLCA (Typed Lambda Calculi and Applications) conference held at Krakow in May. Some interesting material (including the slides of invited talks) are available from the conference web page TLC 2001.

• 12 June Colin Stirling <cps@dcs.ed.ac.uk>

  A Chomsky hierarchy of transition graphs

  I will talk about classes of infinite transition graphs, and so there will be lots of pictures. I will mention a new result, joint with Christophe Morvan (from IRISA in Rennes), relating context-sensitive languages and rational graphs that is to be presented at MFCS 2001.

• 29 May Ian Stark <stark@dcs.ed.ac.uk>
  
  Local areas and the pi-calculus

  Tom Chothia and I have just submitted a paper on using the pi-calculus to express the behaviour of names which are known universally but always refer to local information. This happens, for example, with shared libraries, Java applets, and some internet protocols. I'll talk about the "local area pi-calculus" we use to model this, and an encoding into plain pi-calculus using ethers.

• 1 May John Longley <jrl@dcs.ed.ac.uk>
  
  Getting at the computation strategy behind an ML program

  For the last four weeks I have been trying weeks to implement my latest crazy higher-type operation in New Jersey SML, and on Friday I finally got it working. I will explain what it does from an ML programmer's perspective, and consider some of the slightly surprising things you can do with it. For example, you can debug your ML program with the help of an interactive execution tracer, or optimize it with the help of a generic memoizer. Live demo to be included if I can get the data projector working!

• 24 April Kyriakos Kalorkoti <kk@dcs.ed.ac.uk>
  
  Computing resultants and u-resultants

  Given n forms in n unknowns over an algebraically closed field their resultant tells us if they have a common root (in projective space). One of the best ways to compute the resultant is to use Macaulay's method (which I discussed in an earlier talk). Unfortunately there are exceptional cases that lead to attempts to divide by zero. One way round this was introduced by Cany. The first part of this talk introduces a new way round the difficulty.
  If we have n-1 forms in n unknowns then they are guaranteed to have have comon roots. The u-resultant tells us if there are finitely or infinitely many. Moreover if the first case holds then it also gives us the multiplicities of the roots and (in principle aty least) gives us the roots. Once again there is an approach to computing the u-resultant due to Macaulay but it can suffer from exceptional cases. The rest of the talk will introduce a new approach that avoids these problems.

• 17 April Julian Bradfield <jcb@dcs.ed.ac.uk>
  
  BCTCS Report

  Report on BCTCS 17 (17th British Colloquium for Theoretical Computer Science). For more information see BCTCS 17.

• 27 March Marcelo Fiore <Marcelo.Fiore@cl.cam.ac.uk>
  
  A Piece of Category Theory Motivated by a Combinatorial Identity

• 20 March Massimo Felici <mas@dcs.ed.ac.uk >
  
  Circular Phenomena, Hypersets and Tableaux

  This non-well-founded talk will show:

  • some examples of circular phenomena
  • a brief introduction to Hyperset Theory (Barwise and Moss, 1996; Aczel 1988)
  • a (decidable) Tableaux System for a fragment of the Hyperset Theory (Felici, 1995)
  • a final discussion on possible applications and extensions.
• 13 March Massimo Felici <mas@dcs.ed.ac.uk >
  
  Design for Dependability: Requirements Evolution

  I will give a brief introduction to Dependability. Then I will link the concept of Dependability to that of Requirements Evolution. The link is expressed by means of some industrial case studies. The discussion of practical issues may identify some interesting theoretical discussions.

• 6 March Masahito Hasegawa <mhas@dcs.ed.ac.uk>
  
  A Worst-case Analysis of Cube-like Puzzles

  We give an elementary proof of the following fact (with several variations): you need at least 21 moves to solve Rubik's Cube if you are unlucky.

• 27 February Jung-Bae Son < jun@dcs.ed.ac.uk >
  
  Path-coupling for Lozenge-tilings

  In statistical physics lozenge-tilings can be used to describe monomer-dimer configurations, thus one is interested in sampling such tilings efficiently. It has empirically been known that Markov chain algorithms deliver an efficient way of sampling such structures but a rigorous proof was lacking. Luby, Randall and Sinclair designed a Markov chain for generating random Lozenge-tilings and showed its rapid mixing using a coupling argument. Instead of following their argument, the same result can be obtained by applying path-coupling, which gives a slightly simpler proof. In contrast to coupling, where all states of the chain have to be coupled, with path-coupling only states of a (often rather arbitrarily chosen) set of neighbouring states need to be coupled making finding an appropriate coupling much easier.

• 20 February Eric Vigoda < vigoda@dcs.ed.ac.uk >
  
  A Gentle Introduction to the Markov Chain Monte Carlo Method

  I'll give a gentle introduction to the Markov chain Monte Carlo method, including some techniques such as coupling. This will bring everyone up to steam for the afternoon's theory seminar by Martin Dyer as well as the additional theory seminar at the end of the week by me.
  
  

• 6 February Masahito Hasegawa <mhas@dcs.ed.ac.uk>
  
  Report on the Third ACM SIGPLAN Workshop on Continuations (CW'01)

  I shall give a report on the talks given at CW'01, a satellite event of the 28th POPL held in London last month. There were eight talks (including one invited talk). The topics could be classified into (roughly) three categories:

  • Continuation Passing Style (CPS) transformations (4 talks)
  • typing of the first-class control operators (3 talks)
  • applications (1 talk)
  Based on this classification, I shall try to give an overview of these talks.
• 30 January Samuel Lindley <samuel@dcs.ed.ac.uk>
  
  Report on POPL and FOOL workshop

  I recently attended POPL (Principles of Programming Languages) and the FOOL (Foundations of Object-Orientated Languages) workshop. I shall give a report on a few of the talks:

  • Subtyping Arithmetical Types (Joseph Gil)
  • Typing a Multi-Language Intermediate Code (Andrew Gordon and Don Syme)
  • Fickle: Dynamic Object Reclassification (Sophia Drossopoulou et al.)
  • A Recipe for Raw Types (Benjamin Pierce et al.)
• 23 January Martin Hofmann <mxh@dcs.ed.ac.uk>
  
  Trip report on Programming Methodology Working Group Meeting and SPACE workshop

  Last week I attended a meeting by the IFIP working group 2.3 (programming methodology) and the SPACE (Semantics, Program Analysis, and Computing Environments for Memory Management) workshop. I'd like to report on some of the talks, among them:

  • Ken McMillan, Using model checking for theorem proving: He has managed to verify Tomasulo's algorithm in a "few dozen lines" using clever abstractions and model checking. Compare this to Pnueli's proof presented here a year or so ago.
  • Greg Nelson, Generating near-optimal code automatically: Uses AI ideas and SAT solver to generate optimised code for small basic blocks. One example: code for rearranging bits in a 32bit word used in translation from one platform to another. Ordinary compiler does it in 7 cycles, clever engineer thinking about it for 2 days manages to cut this down to 6 cycles and so does the new method.
  • Mads Tofte, Experiences with region-based memory management: Main conclusion: Relying entirely on inference might not be such a good idea after all. Need to give the programmer some explicit control over MM.
  • Anders Moller, Verification of datatype implementations with graph types and monadic second order logic: A graph type is a generalisation of recursive types for which monadic second order logic is still decidable. Examples of graph types are doubly-linked lists or trees with extra pointers joining their entries in a linked list. The authors define a Hoare logic and decision procedure based on this.

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