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
16:15-17:00
Membrane Computing
17:00-17:45
Total Parser Combinators
from 17:45 Pub and Restaurant
Please use the following links to find
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'.
Marian Gheorghe (Sheffield)
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.
Travel
The seminars will take place at:
Lecture Theatre SG-LT07
Sir Frederick Mappin Building
Mappin Street
Sheffield S1
United Kingdom
Walking from Sheffield Train Station to Mappin Building takes about 20 minutes.
