Midlands Graduate School in the Foundations of Computing Science

Christmas Seminars

Tuesday 15.12.2009, 14.00-17.45
Sir Frederick Mappin Building, SG-LT07
The University of Sheffield



This year's Christmas Seminars are hosted by the Department of Computer Science at the University of Sheffield.
Please contact Georg Struth for all enquiries and visit this site again for updates.


14:00-15:00    Proving that programs eventually do something good
     Byron Cook (Microsoft Research Cambridge and Queen Mary, London)

Software failures can be sorted into two groups: those in which something bad happens (e.g. crashes), and those that in which the intended effect never occurs (e.g. hangs). In recent years automatic tools have been developed which use mathematical proof techniques to certify that certain bad events cannot happen. Methods of establishing the absence of hangs, however, have remained open. In fact---based on Alan Turing's proof of the halting problem's undecidablity---many have considered the dream of automatically proving the absence of hangs to be impossible. While not refuting Turing's original result, recent research now makes this dream a reality. This lecture will describe the recent work.

15:00-15:30    Coffee

15:30-16:15   On Universal Algebra over Nominal Sets
     Alexander Kurz (Leicester)

(Joint work with D. Petrisan) We study universal algebra over Nom, the category of nominal sets in the sense of Gabbay and Pitts. Whereas Nom, and categories of algebras over Nom, do not form varieties in the sense of universal algebra, it is possible to study them by investigating the varities induced by them. For example, we show how to obtain an HSP theorem for nominal algebras from Birkhoff's HSP theorem of universal algebra. This theorem is different from the one proposed by Gabbay, and we recover his theorem by restricting the equational logic of universal algebra to what we call `uniform equations'.

16:15-17:00   Membrane Computing
     Marian Gheorghe (Sheffield)

17:00-17:45   Total Parser Combinators
     Nils Anders Danielsson (Nottingham)

Parser combinators provide an elegant method for implementing parsers. However, most parser combinator libraries fail to guarantee that parsing will terminate. I will talk about a library which provides such a guarantee. The library's interface is similar to that of many other parser combinator libraries, with three main differences: one is that the interface clearly specifies which parts of the constructed parsers may be infinite, and which parts have to be finite, using a combination of induction and coinduction; another is that the interface allows many forms of left recursion; and the last is that the parser type is unusually informative. The parser combinators come with a formal semantics, and are as expressive as possible: every language which can be decided by the host language can also be decided using the combinators.

from 17:45   Pub and Restaurant


The seminars will take place at:

Lecture Theatre SG-LT07
Sir Frederick Mappin Building
Mappin Street
Sheffield S1
United Kingdom

Please use the following links to find

Walking from Sheffield Train Station to Mappin Building takes about 20 minutes.

University Crest