Sir Frederick Mappin Building, SG-LT07

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*

Lecture Theatre SG-LT07

Sir Frederick Mappin Building

Mappin Street

Sheffield S1

United Kingdom

Please use the following links to find

- information for visitors, including maps and travel advice;
- a campus map (Mappin Building has number 170);
- a route planner.