THEORY (OLD) SEMINARS NOTE: Seminars in this series prior to Spring 2004 are listed on a separate archive page. Visit http://events.cs.bham.ac.uk/news/seminar-archive/theorysem for more information. -------------------------------- Date and time: Friday 23rd January 2004 at 14:00 Location: UG40, School of Computer Science Title: Organismic and Evolutionary Biology, Harvard University Speaker: Richard Watson Institution: Harvard University, USA Abstract: Evolutionary Computation, EC, has developed largely in isolation from the Evolutionary Biology, EB, that inspired it and each discipline treats the subject of sexual recombination, or crossover, quite differently. Formal population genetics models in EB treat sexual recombination as a mechanism that forces selection to act on the average fitness effect of individual alleles and this reinforces the conception of evolution as a simple hill-climbing process. In contrast, EC is generally more interested in the ways that an evolutionary algorithm might differ from the behaviour of a simple hill-climber, and somewhat paradoxically, it is recombination, and its ability to exchange sets of tightly linked coadapted alleles as a unit, that is implicated here. Recent results in EC have shown cases where a recombining population can evolve fit genotypes that cannot be evolved with a hill-climber, but these models have been rather complex. In this talk I build upon earlier results in EC to devise a simple two-module epistatic model which helps to clarify the potential of recombination in EC. This model is also consistent with common knowledge of genetics and simple enough to facilitate comparison with population genetic models. This work thereby recombines results from EC with EB theory, and appropriately enough, uses the topic of sexual recombination to do so. -------------------------------- Date and time: Friday 30th January 2004 at 14:00 Location: UG40, School of Computer Science Title: Canonical models for computational effects Speaker: John Power Institution: University of Edinburgh Abstract: Given a signature of basic operations for a computational effect such as side-effects, interactive input/output, or exceptions, we give a unified construction that determines equations that should hold between derived operations of the same arity. We then show how to construct a canonical model for the signature, together with the first-order fragment of the computational lambda-calculus, subject to the equations, done at the level of generality of an arbitrary computational effect. We prove a universality theorem that characterises the canonical model, and we outline how to extend such models to the full computational lambda-calculus. Our leading example is that of side-effects, with occasional reference to interactive input/output, exceptions, and nondeterminism. -------------------------------- Date and time: Friday 6th February 2004 at 14:00 Location: UG40, School of Computer Science Title: When is a difference not a difference? Why Penrose fails to prove the impossibility of AI Speaker: Ron Chrisley Institution: University of Sussex Abstract: In two widely-read books, Roger Penrose resuscitated an old argument (originally considered by Gödel, Turing and Lucas) against the possibility of formalising human thought. The argument is essentially logico-mathematical, drawing on principles used in Cantor's diagonal argument and Gödel's incompleteness theorem. Unlike other commentators, I propose that while the formal argument Penrose presents is sound and valid, the informal, sceptical conclusion concerning AI that he draws from it is a non-sequitur. While it might be true that there are computations we can perform that no Turning machine can, this does not imply that there are aspects of human cognition that are not simulable by any Turing Machine. -------------------------------- Date and time: Friday 20th February 2004 at 14:00 Location: UG40, School of Computer Science Title: A hyperset approach to semistructured or Web-like databases Speaker: Vladimir Sazonov Institution: University of Liverpool Abstract: Since 1970, when E.F. Codd introduced the relational approach to databases, Relational Databases have become the mainstream both in database theory and in the industry of database management systems. This is one of the brightest examples of the influence of mathematics and mathematical logic (where relation is also a fundamental concept) on computer practice. Now a new idea of semistructured databases (SSD) has arisen. It does not fit well with the relational approach although it is usually presented in terms of edge labelled graphs which are mathematically just two column relational tables (with labelled rows). The point is that some other kind of issues with such graphs arises which are not so "relational". The Hyperset approach to SSD is intimately connected with the graph approach and is, in fact, a natural generalization of the relational approach. The idea is extremely simple, but abstract. Each vertex X of a graph is considered as a (hyper)set name and generates a set equation X = {l_1:X_1,...,l_n:X_n} where l_i:X -> X_i are all outgoing l_i-labelled edges. According to the (non-wellfounded) Hyperset Theory (from a book of P.Azcel or another book of J. Barwise and L. Moss) each such system of set equations generated by a graph has a unique solution in the universe of (abstract) hypersets. Each hyperset X is a set of labelled sets of sets of sets, etc., possibly with cycles (according to the given graph). Thus, graph vertices only represent hypersets. These are hypersets which are considered as (abstract) SSD states (like relations which are also sets of tuples). Any query to SSD in this approach is just an operation over hypersets (like operations over relations in the relational approach to databases), whereas graphs or, equivalently, systems of set equations representing hypersets and SSDs serve to compute these abstract operations/queries by appropriate (restructuring and bisimulation invariant) graph transformers. A hyperset query language Delta will be discussed whose expressive power proves to be exactly PTIME (also for the case of multi-hypersets). Some variations of Delta for the case of acyclic graphs (sets) have expressive power (N/D)LOGSPACE. No such results are known to the author for purely graph approaches to SSD. Any SSD, as a system of hyperset equations, may be divided into parts and represented as, say, HTML files distributed potentially over the world with each set name X_i "clickable" and leading to the (possibly remote) file with the corresponding equation X_i={...}. This, as well as the arbitrary graph structure of SSD, suggests calling such databases Web-like (WDB). Thus, in principle, the Delta-language can be considered as a powerful, flexible and restructuring (unlike the usual querying mechanisms of, e.g., Google) query language to WDB or even to WWW. Some implementation issues potentially leading to a WDBMS, (like many existing RDBMS) for example, multiple mobile agent execution of Delta queries will be discussed, too. This talk is based on joint works with my colleagues Alexei Lisitsa, Alexandr Leontjev and Yuri Serdyuk. -------------------------------- Date and time: Friday 5th March 2004 at 14:00 Location: UG40, School of Computer Science Title: Resources, Concurrency and Local Reasoning Speaker: Peter O'Hearn (http://www.dcs.qmw.ac.uk/~ohearn/) Institution: Queen Mary, University of London (http://www.dcs.qmw.ac.uk/) Host: Uday Reddy Abstract: We show how a resource-oriented logic, separation logic, can be used to reason about the correct use of resources in concurrent programs. -------------------------------- Date and time: Friday 12th March 2004 at 14:00 Location: UG40, School of Computer Science Title: Adjunction Models For Call-By-Push-Value With Stacks Speaker: Paul Levy (http://www.cs.bham.ac.uk/~pbl) Institution: The University of Birmingham () Host: Volker Sorge Abstract: Call-by-push-value is a "semantic machine code", providing a set of simple primitives from which both the call-by-value and call-by-name paradigms are built. We present its operational semantics in the form of a stack machine, and see how this machine suggests a term judgement of stacks. We then see that CBPV, incorporating these stack terms, has a simple categorical semantics based on an adjunction. We describe this semantics incrementally. First, we introduce locally indexed categories and the opGrothendieck construction, and use these to give the basic structure for interpreting the 3 judgements: values, stacks and computations. Then we look at the universal property required to interpret each type constructor. We define a model to be a strong adjunction with countable coproducts, countable products and exponentials. We see a wide range of instances of this structure: we give examples for divergence, storage, erratic choice, continuations, games (with or without a bracketing condition) etc., in each case resolving the familiar strong monad (as advocated by Moggi) into a strong adjunction. -------------------------------- Date and time: Friday 19th March 2004 at 14:00 Location: UG40, School of Computer Science Title: Call-by-value is dual to call-by-name Speaker: Phil Wadler (http://homepages.inf.ed.ac.uk/wadler/) Institution: University of Edinburgh (http://www.inf.ed.ac.uk/) Host: Paul Levy Abstract: The rules of classical logic may be formulated in pairs corresponding to De Morgan duals: rules about "and" are dual to rules about "or". A line of work, including that of Filinski (1989), Griffin (1990), Parigot (1992), Danos, Joinet, and Schellinx (1995), Selinger (1998,2001), and Curien and Herbelin (2000), has led to the startling conclusion that call-by-value is the de Morgan dual of call-by-name. This paper presents a dual calculus that corresponds to the classical sequent calculus of Gentzen (1935) in the same way that the lambda calculus of Church (1932,1940) corresponds to the intuitionistic natural deduction of Gentzen (1935). The paper includes crisp formulations of call-by-value and call-by-name that are obviously dual; no similar formulations appear in the literature. The paper gives a CPS translation and its inverse, and shows that the translation is both sound and complete, strengthening a result in Curien and Herbelin (2000). Paper -------------------------------- Date and time: Friday 26th March 2004 at 14:00 Location: UG40, School of Computer Science Title: Execution of Large Scale HLA-Based Distributed Simulations over the Grid Speaker: Stephen J. Turner (http://www.ntu.edu.sg/home/assjturner/) Institution: Nanyang Technological University, Singapore (http://sentosa.sas.ntu.edu.sg:8000/) Host: Georgios Theodoropoulos Abstract: Modeling and simulation is required in many areas of science, engineering and commerce, e.g., for predicting the behavior of systems being designed or for analyzing and optimizing existing systems. These complex simulations often require huge computing resources and the data sets required may also be geographically distributed. In order to cater for the increasing complexity of the simulation systems, it is necessary to harness computing power over the Internet. While the High Level Architecture (HLA) defines a standard for the construction of distributed simulations, Grid technology enables the use of distributed computing resources and also facilitates access to geographically distributed data sets. To meet the performance requirement demanded by large-scale distributed simulations, resource management mechanisms that balance the load and provide fault-tolerance capability are desired. In addition, to conduct simulation experiments easily over distributed resources from different organizations, mechanisms that can deploy coordinated and secured simulation executions are required. In this talk, initial work on the execution of large-scale HLA-based distributed simulations over the Grid will be discussed. -------------------------------- Date and time: Friday 16th April 2004 at 14:00 Location: UG40, School of Computer Science Title: new-HOPLA --- a higher-order process language with name generation Speaker: Francesco Zappa Nardelli (http://www.di.ens.fr/~zappa/) Institution: University of Cambridge (http://www.cl.cam.ac.uk) Host: Martin Escardo Abstract: We introduce new-HOPLA, a concise but powerful language for higher-order nondeterministic processes with name generation. Its origins as a metalanguage for domain theory are sketched but for the most part we concentrate on its operational semantics. The language is typed, the type of a process describing the shape of the computation paths it can perform. Its transition semantics, bisimulation, congruence properties and expressive power are explored. We give encodings of well-known process algebras, including pi-calculus and Higher-Order pi-calculus. This is joint work with Glynn Winskel (Computer Laboratory, University of Cambridge) -------------------------------- Date and time: Friday 7th May 2004 at 11:00 Location: UG40, School of Computer Science Title: Domain theoretical models of linear polymorphism Speaker: Paola Maneggia (http://www.cs.bham.ac.uk/~pxm) Institution: The University of Birmingham (http://www.cs.bham.ac.uk) Host: Achim Jung Abstract: We give a construction to get a model of linear logic with second order universal quantification starting from a suitable linear category of domains (such as the category of prime algebraic lattices and functions preserving arbitrary suprema). Key ingredients are lax transformations, lax limits and bifiniteness. This construction also accounts for the Coquand-Gunter-Winskel model of System F based on Scott-domains. -------------------------------- Date and time: Monday 17th May 2004 at 15:00 Location: 217, School of Computer Science Title: Verifying Product-Line Systems Speaker: Kathi Fisler (http://www.cs.wpi.edu/People/faculty/kfisler.html) Institution: Worcester Polytechnic Institute, USA (http://www.cs.wpi.edu/) Host: Mark Ryan Abstract: Feature-oriented programming organizes programs around features rather than objects, thus supporting extensible, product-line architectures. Programming languages increasingly support this style of programming, but programmers get little support from verification tools. Ideally, programmers should be able to verify features independently of each other and use automated compositional reasoning techniques to infer properties of a system from properties of its features. Unfortunately, most modular model checking techniques do not support feature-oriented modules; they betray their hardware roots by assuming that modules compose in parallel. In contrast, feature-oriented modules compose sequentially in the simplest case; most interesting feature-oriented designs are really quasi-sequential compositions of parallel compositions. These designs therefore demand and inspire new verification techniques. This talk gives an overview of feature-oriented modules, our compositional model checking methodology for them, and its application to real software systems. -------------------------------- Date and time: Friday 21st May 2004 at 14:00 Location: UG40, School of Computer Science Title: A formal framework for the development of secure systems Speaker: Helge Janicke and Francois Siewe (http://www.cse.dmu.ac.uk/~fsiewe/) Institution: De Montford University (http://www.dmu.ac.uk) Host: Dimitar Guelev and/or Mark Ryan Abstract: With the increasing complexity of distributed systems, security-concerns gain more and more importance. The development of these systems need to be focused on security. We base our formal approach for the design of security critical systems on Interval Temporal Logic (ITL) and provide a framework that allows to specify security, functional and temporal requirements in a uniform way. This talk will give an introduction to ITL and show how security policies, such as authorisation, delegation and obligation policies can be expressed. We then present a rich set of operators for composing and dynamically enforcing policies. The last part of this talk decribes the design language SANTA that allows to integrate security policy and functionality. -------------------------------- Date and time: Friday 28th May 2004 at 14:00 Location: UG40, School of Computer Science Title: MathLang: A language for Mathematics Speaker: Fairouz Kamareddine (http://www.macs.hw.ac.uk/~fairouz/) Institution: Heriot-Watt University (http://www.macs.hw.ac.uk/) Host: Alan Sexton Abstract: Frege was frustrated by the use of natural language to describe mathematics. In the preface to his Begriffsschrift he says: "I found the inadequacy of language to be an obstacle; no matter how unwieldy the expressions I was ready to accept, I was less and less able, as the relations became more and more complex, to attain the precision that my purpose required." Frege therefore presented in his Begriffsschrift, the first extensive formalisation of logic giving logical concepts via symbols rather than natural language. Frege developed things further in his Grundlagen and Grundgesetze der Arithmetik which could handle elementary arithmetic, set theory, logic, and quantification. In his Grundlagen der Arithmetik, Frege argued that mathematics can be seen as a branch of logic. In his Grundgesetze der Arithmetik, he described the elementary parts of arithmetic within an extension of the logical framework of Begriffsschrift. Frege's tradition was followed by many others: (Russell, Whitehead, Ackermann, Hilbert, etc.). Russell discovered a paradox in Frege's work and proposed type theory as a remedy. Advances were also made in set theory, category theory, etc., each being advocated as a better foundation for mathematics. But, none of the logics proposed satisfies all the needs of mathematicians. In particular, they do not have linguistic categories and are not a satisfactory communication medium. Moreover: * Logics make choices (types/sets/categories, predicative/impredicative, etc.). But different parts of mathematics need different choices. There is no agreed best formalism. * A logician's formalization of a {sc Cml} text loses the original structure and is thus of little use to ordinary mathematicians. * Mathematicians can do their work without formal mathematical logic. In the second half of the twentieth century, programming languages were being developed and this led to the creation of softwares, systems and tools to computerize and check mathematics on the computer, and to give some help and assistance to teachers, students, and users of mathematics. But, a mathematical text is structured differently from a machine-checked text proving the same facts. Making the latter involves extensive knowledge and many choices: * The Choice of the underlying logic. * The Choice of how to implement concepts (equational reasoning, induction, etc.). * The Choice of the formal system: a type theory (which?), a set theory (which?), etc. * The Choice of the proof checker: Coq, Isabelle, PVS, Mizar, etc. Furthermore, checking mathematics on the computer has other problems: * An informal mathematical proof will cause headaches as it is hard to turn in one big step into a (series of) syntactic proof expressions. * During the checking of mathematics, the informal proof is replaced by a complete proof where every detail is spelled out. Very long expressions replace the clear mathematical text and this is useless to ordinary mathematicians. * so, despite the enourmous work on logics for mathematics as in Frege's tradition, and computer tools and systems for implementing and checking mathematics as in the second half of the twentieth century, mathematicians remain sceptical about using logic and using computers. In this talk, I argue that both the logic for mathematics and the computation of mathematics have forgotten the mathematician and the language of mathematics during their development. I start from de Bruijn's mathematical vernacular which he refined almost twenty years after the begin of his Automath project (Automating Mathematics). I compare this vernacular to modern approaches for putting mathematics on the computer (e.g., OMDOC, MathML, versions of XML, etc.) and discuss how we can find a language of mathematics that is open to future developments through logic and computation. -------------------------------- Date and time: Tuesday 8th June 2004 at 15:00 Location: UG40, School of Computer Science Title: Herman's Ring: a program-logic analysis Speaker: Carroll Morgan (Joint work with Annabelle McIver) Host: Marta Kwiatkowska Abstract: Herman's Ring is a self-stabilising distributed protocol, dating from 1990, that has been much analysed and targeted as a test-bed for approaches to reasoning about probabilsitic algorithms. In this talk I will use it to illustrate an extremely simple and effective technique for proving probability-one termination. Although based on classical techniques from probability theory (zero-one laws), and having been introduced to computer science by Hart, Sharir and Pnueli in the early 1980's, the method still deserves to be more widely known. Our contribution is to embed the technique in a probabilistic program logic (and to prove it there). In addition, if there is time, I will discuss a new result --- that Herman's Ring has expected time complexity of THETA(N^2) --- which also uses program-logic techniques in its proof (as opposed eg to reasoning operationally over automata or Markov chains directly). -------------------------------- Date and time: Friday 25th June 2004 at 14:00 Location: UG40, School of Computer Science Title: Generating, Creating, Proving, and Distributing Speaker: Volker Sorge (http://www.cs.bham.ac.uk/~vxs) Institution: School of Computer Science, The University of Birmingham (http://www.cs.bham.ac.uk) Host: Himself Abstract: or Why "Theory People" use the Cluster Classifying finite algebraic structures has been a major motivation behind much research in pure mathematics. Automated techniques have aided in this process, but this has largely been at a quantitative level, e.g., to prove that there are no quasigroups of a given type for a given size, or to count the number of groups of a particular order. In contrast, I shall present an approach to produce and verify qualitative theorems, which classify algebras of a particular type and size into isomorphism classes. For a simple example, our system produces and verifies the following (paraphrased) theorem: ``up to isomorphism there are two groups of size 6: one Abelian, one non-Abelian''. This has been achieved by the integration (and improvement) of a number of automated reasoning techniques: we use the model generator to produce examples of the finite algebras, the machine learning systems to generate a classification theorem, and theorem proving to independently prove the correctness of the theorem, as well as a computer algebra system to reduce the complexity of the problems. We have devised a fully automated bootstrapping algorithm for taking the axioms of an algebra and producing a decision tree embedding a fully verified classification theorem. The power of this approach is demonstrated by producing new classification theorems for non-associative algebras of various sizes. The performance of the bootstrapping algorithm can be improved by introducing parallelisation and distribution at various points. Moreover, we have contrived a technique that reuses constructed decision trees for informed distributed model generation. This is joint work with Simon Colton, Andreas Meier and Roy McCasland. -------------------------------- Date and time: Friday 9th July 2004 at 14:00 Location: UG05, Learning Center Title: Language inclusion for timed automata: closing a decidability gap Speaker: James Worrell (http://www.math.tulane.edu/~jbw/) Institution: Tulane University, USA (http://www.math.tulane.edu/) Host: Marta Kwiatkowska Abstract: The algorithmic analysis of timed automata is fundamentally limited by the undecidability of the language inclusion problem (given two timed automata A and B, are all the timed traces accepted by B also accepted by A?). In this talk, we show that, if A is restricted to having a single clock, the problem becomes decidable. This is somewhat surprising, since it is well-known that there exist timed automata with a single clock that cannot be complemented. The crux of our proof consists in reducing the language inclusion problem to a reachability question on an infinite labeled transition system; we then construct a suitable well-quasi-ordering on this state space, which ensures the termination of our search algorithm. This is oint work with Joel Ouaknine, CMU. -------------------------------- Date and time: Friday 3rd September 2004 at 14:00 Location: UG40, School of Computer Science Title: Architectural Constraints on Complex Learning Systems Speaker: L. Andrew Coward (http://cs.anu.edu.au/~Andrew.Coward/) Institution: Department of Computer Science, Australian National University (http://cs.anu.edu.au/) Host: Aaron Sloman Abstract: The architectural form of any system which performs a large number of interacting control features is strongly influenced by the need to perform all its features with limited information handling resources combined with the need to make ongoing modifications to some operational features without side effects on other features. Given great enough operational complexity relative to available resources, these needs constrain such systems within specific architectural bounds. One such bound is separation of system operations into modular hierarchies in which modules perform groups of similar operations on shared information handling resources and do not correspond with features. The requirement to maintain adequate operational meanings for information exchanged between modules results in additional architectural bounds. If such meanings are unambiguous, these bounds correspond with the classical von Neumann architecture, and learning of complex combinations of operations is impractical. If such meanings are partially ambiguous, learning is possible and system architectural form is constrained within a set of bounds called the recommendation architecture. These bounds limit overall structure, detailed substructures, algorithms and processes in a number of specific ways. Electronic implementations confirm the learning capabilities of systems within the recommendation architecture bounds and in particular the ability to learn without interference with prior learning. Since the human brain must learn a complex combination of interacting cognitive capabilities, and its information handling capabilities are not unlimited, it will be constrained within the recommendation architecture bounds. The psychological and physiological evidence for these bounds in the human brain will be briefly discussed. -------------------------------- Date and time: Friday 1st October 2004 at 14:00 Location: UG40, School of Computer Science Title: TBA Speaker: Richard Dearden (http://is.arc.nasa.gov/AR/tasks/PrbDet.html) Institution: NASA Ames Research Center, USA (http://is.arc.nasa.gov/) Host: Aaron Sloman -------------------------------- Date and time: Friday 8th October 2004 at 14:00 Location: UG40, School of Computer Science Title: Moving Towards Self-Managing Systems Speaker: Christine Draper (mailto:DRAPERC@uk.ibm.com) Institution: IBM Hursley labs (http://www-306.ibm.com/autonomic/library.shtml) Host: Padma Reddy and Mark Ryan Abstract: The IT industry has spent decades creating computer systems with ever-increasing degrees of complexity to solve a wide variety of business problems. Ironically, complexity itself has become part of the problem. As networks and distributed systems grow and change, they can become increasingly hampered by system deployment failures, hardware and software issues, not to mention human error. Autonomic computing was conceived as a way to help reduce the cost and complexity of owning and operating an IT infrastructure, using technology to manage technology. The idea is not new many of the major players in the industry have developed and delivered products based on this concept. This talk provides an overview of IBM's autonomic computing architecture and two of its core technologies (problem determination and solution installation), as well as some examples of how autonomic features are being implemented in IBM products. Christine Draper is a Senior Technical Staff Member at IBM's UK Laboratory in Hursley, Winchester. She is a lead architect in IBM's Autonomic Computing team, with responsibility for the architecture and core technology for self-configuration, including solution installation. -------------------------------- Date and time: Friday 15th October 2004 at 14:00 Location: UG40, School of Computer Science Title: A Category-theoretic Framework for Comparing Evolutionary Algorithms via Their Representation Speaker: Boris S Mitavskiy (mailto:B.S.Mitavskiy@cs.bham.ac.uk) Institution: School of Computer Science (http://www.cs.bham.ac.uk) Abstract: In this talk I shall introduce an appropriate mathematical notion of what it means to re-encode one evolutionary algorithm by another. In fact, I shall introduce a certain category, the morphisms of which are intuitively thought of as re-encoding functions. It turns out that these morphisms are related to the family of the so-called recombination-invariant subsets in a similar way as continuous maps are related to the family of open sets and measurable functions are related to the $sigma$-algebra of measurable sets. This allows us to classify all possible re-encodings of a given evolutionary search algorithm in terms of a classical genetic algorithm. Moreover, we are able to construct the best possible "coarse graining" of a given evolutionary algorithm to make it imbeddable into a binary genetic algorithm in terms of the left adjoint to an appropriate forgetful functor. -------------------------------- Date and time: Friday 22nd October 2004 at 14:00 Location: UG40, School of Computer Science Title: Permissions, concurrency, resourcing: a breakthrough and Grand Challenge Speaker: Richard Bornat (http://www.cs.mdx.ac.uk/staff/profiles/r_bornat.html) Institution: School of Computer Science, Middlesex University (http://www.cs.mdx.ac.uk/) Host: Uday Reddy Abstract: Separation logic began as a treatment of programs which worked on independent areas of the store. We've now found how to describe and reason about sharing, ownership transfer and concurrency primitives like semaphores and conditional critical regions. We think we have a new take on critical sections, which we can treat formally. There are problems which we are still struggling with: there seems to be more than one model, matching more than one kind of sharing/separation; we haven't quite conquered sharing and ownership of variables; we haven't mechanised our logic. Nevertheless, we think we have punched a very big hole in the walls of the problem of safe concurrent programming through which we can drive quite a lot of logical tanks. The overall purpose of this work is to facilitate _resourcing_, a step beyond typing which will allow static analysis of programs to ensure they don't overstep their resource bounds. It's a Grand Challenge for formalists, the next big step forward in our mission to make programming more reliable. For those who like proof theory and exciting speculation, I'll give a glimpse of a possible treatment of variables-as-resource. -------------------------------- Date and time: Friday 5th November 2004 at 14:00 Location: UG40, School of Computer Science Title: Approximating set-based structures in topological ones Speaker: Alexander Kurz (http://www.cs.le.ac.uk/~akurz/) Institution: University of Leicester, Department fo Computer Science (http://www.cs.le.ac.uk/) Abstract: The title is taken from Abramsky's "A domain equation for bisimulation" (1991) where, at the end, the comparison of coalgebras for the `same' functor on different (topological) base categories is suggested. I will discuss some further instances of this situation and present some related results and methods from modal logic. -------------------------------- Date and time: Friday 19th November 2004 at 14:00 Location: UG40, School of Computer Science Title: Clash with other school activities Speaker: Slot not available -------------------------------- Date and time: Friday 26th November 2004 at 14:00 Location: UG40, School of Computer Science Title: Towards a Geometry of Realizability Toposes? Speaker: Prof. Peter T. Johnstone (http://www.dpmms.cam.ac.uk/site2002/People/johnstone_pt.html) Institution: Cambridge University, Department of Pure Mathematics and Mathematical Statistics (http://www.dpmms.cam.ac.uk/) Host: Martin Escardo, Achim Jung and Steve Vickers Abstract: The notion of realizability topos has been around for over tewnty years now: numerous variants of the basic construction of a topos from a Schoenfinkel algebra (or PCA) have been studied, and many different examples of Schoenfinkel algebras have been considered. However, until recently (with the notable exception of John Longley's Ph.D. thesis) there has been relatively little work on how these different examples fit together: we do not have a well- understood 2-category of realizability toposes in the same way that we have a well-understood 2-category of Grothendieck toposes. I believe that the time is now ripe for the development of such an understanding: in this talk I shall attempt to give some indications of what we already know, and what we might hope to learn, about morphisms between realizability toposes. -------------------------------- Date and time: Friday 3rd December 2004 at 14:00 Location: UG40, School of Computer Science Title: Formal Security Analysis of Mobile Ad-Hoc Networks Speaker: Sebastian Nanz (http://www.doc.ic.ac.uk/~nanz/) Institution: Department of Computing, Imperial College London (http://www.doc.ic.ac.uk/) Abstract: Mobile Ad-Hoc Networks are wireless, mobile, multi-hop networks that operate without existing infrastructure except for the participating nodes and their computing capabilities. Their specific characteristics raise a number of security issues which are not solved by traditional security designs. Likewise, formal techniques are challenged to find flaws in new protocol designs or prove them correct, but the highly dynamic nature of these networks poses a major difficulty for their modelling and analysis. In this talk, we present a process calculus framework for modelling ad-hoc networks that takes the network topology as an explicit parameter. This enables us to make a clear distinction between process actions and the changing state of communication links, and therefore to model spontaneous topology changes. We show how we can then use this calculus and its extensions to derive security results. -------------------------------- Date and time: Friday 21st January 2005 at 14:00 Location: UG40, School of Computer Science Title: Domain-Theoretic Solutions Initial and Boundary Value Problems Speaker: Dirk Pattinson (http://www.pst.informatik.uni-muenchen.de/personen/pattinso/) Institution: Department of Computer Science, LMU Munich, visiting Imperial College London (http://www.pst.informatik.uni-muenchen.de/) Host: Achim Jung Abstract: By a domain theoretic solution of a differential equation we mean an algorithm that computes Scott continuous, interval valued functions that converge to a solution of the problem. We review already established techniques, and present an extension that directly allows to compute solutions with a maximal domain of definition. We then show, how this method can be employed to solve linear boundary value problems. This lead to an algorithm that computes unique solutions of boundary problems whenever they exist. -------------------------------- Date and time: Friday 11th February 2005 at 14:00 Location: UG40, School of Computer Science Title: The Visitor pattern, type-theoretically! Speaker: Peter Buchlovsky (http://www.cl.cam.ac.uk/users/pb368/) Institution: University of Cambridge Computer Laboratory (http://www.cl.cam.ac.uk/) Host: Hayo Thielecke Abstract: In object-oriented languages, the Visitor pattern is used to traverse tree-like data structures. In this talk, we consider a type-theoretic reconstruction of the Visitor pattern, arising from the encoding of algebraic types into the polymorphic lambda calculus. We give a transformation from a restricted form of F_{omega} to Featherweight Generic Java and show that this can be used to derive the Visitor pattern from our encoding. -------------------------------- Date and time: Friday 25th February 2005 at 14:00 Location: UG40, School of Computer Science Title: Foundations of Modular Structural Operational Semantics Speaker: Peter Mosses (http://www.brics.dk/~pdm/) Institution: Department of Computer Science, University of Wales Swansea (http://www.swan.ac.uk/compsci/) Host: Paul Levy Abstract: Modular SOS (MSOS) is a variant of conventional SOS. Using MSOS, the transition rules for each construct of a programming language can be given incrementally, and they do not need reformulation when further constructs are added to the described language. MSOS thus provides an exceptionally high degree of modularity in semantic descriptions, removing a shortcoming of the original SOS framework. The crucial feature of MSOS is that labels on transitions are now morphisms of a category, and exploited to ensure the appropriate flow of information (such as environments and stores) during computations. The talk explains the foundations of MSOS, and illustrates how MSOS descriptions are written in practice. It also discusses standard notions of semantic equivalence for MSOS, and indicates how MSOS descriptions can be translated to Prolog. Familiarity with the basic ideas of conventional SOS and labelled transition systems is assumed. -------------------------------- Date and time: Friday 18th March 2005 at 14:00 Location: UG40, School of Computer Science Title: Overt solutions of real equations Speaker: Paul Taylor (http://www.cs.man.ac.uk/~pt/) Institution: Department of Computer Science, University of Manchester (http://www.cs.man.ac.uk/) Host: Achim Jung Abstract: Abstract Stone Duality is a revolutionary theory that axiomatises general topology directly, without using either set theory or infinitary lattice theory. Every expression in the calculus denotes both a continuous function and a program. The closed interval is compact, whereas in the Russian school of computable analysis it is not. Nevertheless, the reasoning looks remarkably like a sanitised form of that in classical topology. This paper applies ASD to elementary real analysis, culminating in the Intermediate Value Theorem, ie the solution of equations f x=0 for continuous f:R->R. As is well known from both numerical and constructive considerations, the equation cannot be solved if f ``hovers'' near 0, whilst tangential solutions will never be found. In ASD, both these failures and the general method of finding solutions of the equation when they exist are explained by the new concept of ``overtness''. Overtness, like compactness, is a purely topological concept. It replaces metrical properties such as total boundedness, and cardinality conditions such as having a countable dense subset. It is also related to locatedness in constructive topology and recursive enumerability in recursion theory. Overtness and compactness are expressed by the two modal operators, which may be interpreted as higher-order, parallel, non-deterministic logic programs, which find solutions of equations in a uniform way. -------------------------------- Date and time: Friday 13th May 2005 at 14:00 Location: UG40, School of Computer Science Title: TBA Speaker: Eike Ritter (http://www.cs.bham.ac.uk/~exr) Institution: School of Computer Science (http://www.cs.bham.ac.uk) -------------------------------- Date and time: Friday 27th May 2005 at 14:00 Location: UG40, School of Computer Science Title: Electoral Systems in Ambient Calculi Speaker: Maria Grazia Viglioti Institution: Imperial College Abstract: We compare the expressiveness of ambient calculi against different dialects of the pi-calculus. Cardelli and Gordon encoded the asynchronous pi-calculus into the ambient calculus Mobile Ambients We show that the pure ambient calculus without restriction has symmetric electoral systems, that is, it is possible to solve the problem of electing a leader in a symmetric network. By the work of Palamidessi, this implies that this fragment of the ambient calculus is not encodable (under} certain conditions in the pi-calculus with separate choice. -------------------------------- Date and time: Friday 3rd June 2005 at 14:00 Location: UG40, School of Computer Science Title: A Verifiable Approach to Programming Multi-Agent System Speaker: Rafael Bordini (http://www.dur.ac.uk/r.bordini) Institution: Computer Science, Durham University (http://www.dur.ac.uk/computer.science/) Abstract: This talk will introduce an agent-oriented programming language and some features of its interpreter, then address the use of model-checking techniques for the verification of multi-agent systems implemented in that programming language. The first part of the talk will cover various features of "Jason", a Java-based interpreter for an extended version of a logic-based agent-oriented programming language called AgentSpeak (which is based on the BDI agent architecture). The second part of the talk will overview the research leading to the development of a set of tools which automatically translate AgentSpeak code and a simplified BDI property specification language into the input languages of existing model checkers, thus allowing the verification of multi-agent programs. To address the state-explosion problem, abstraction techniques tailored specifically to that agent-oriented programming language are required. The talk also refers to recent work on a property-based slicing algorithm for AgentSpeak. -------------------------------- Date and time: Friday 15th July 2005 at 14:00 Location: UG40, School of Computer Science Title: Flow Sensitive Security Types Speaker: Sebastian Hunt (http://www.soi.city.ac.uk/~seb/) Institution: City University, London (http://www.soi.city.ac.uk/) Host: Mark Ryan Abstract: For a simple While-language, we present a family of semantically sound information-flow security type systems (parameterized by the choice of security type lattice) which allow the type of a variable to "float", assigning different security types at different points in the program. Choosing security type lattice P(Var) gives a system equivalent to Amtoft and Banerjee's Hoare logic, which derives individual variable-variable independence properties. Surprisingly, for any given choice of security type lattice L, we can show that the fine-grained P(Var)-analysis gives no useful additional precision compared to the simpler L-analysis. We then present a simple type-directed program transformation which transforms any program typable within the floating-type system to an equivalent program typable in a conventional fixed-type system. This is joint work with David Sands and David Clark. -------------------------------- Date and time: Friday 22nd July 2005 at 14:00 Location: UG40, School of Computer Science Title: Proofs, programs and abstract complexity Speaker: Arnold Beckmann (http://www.cs.swan.ac.uk/~csarnold/) Institution: Swansea university (http://www.cs.swan.ac.uk/~csarnold/) Host: Achim Jung Abstract: A meanwhile classical theme in mathematical logic is, that proving forall-exists-statements and defining recursive functions are related concepts. For "classical" theories of arithmetic and corresponding classes of sub-recursive functions, such connections can be obtained, for example, by proof theoretic means. In my talk, I will speak about similar connections between weak theories of arithmetic (called bounded arithmetic [1]) and low level complexity functions (like the polynomial time hierarchy of functions). I will point out how these connections are related to certain abstract measures (called dynamic ordinals [2]) of the provability strength of such theories. In particular, I will mention connections to an enterprise called "Cook's NP versus coNP programme" of proving lower bounds to propositional proof systems. [1] S. Buss: Bounded Arithmetic. Studies in Proof Theory. Lecture Notes, 3. Bibliopolis, Naples, 1986. [2] A. Beckmann: Dynamic ordinal analysis. Arch. Math. Logic 2003, 42: 303-334. -------------------------------- Date and time: Friday 2nd September 2005 at 14:00 Location: UG40, School of Computer Science Title: The RW model-checking framework Speaker: Nan Zhang (http://www.cs.bham.ac.uk/) Institution: School of Computer Science (http://www.cs.bham.ac.uk) Host: Mark Ryan Abstract: We present the RW model-checking framework which is used to evaluate access control policies. The framework contains a modelling formalism (RW formalism), a machine-readable language (RW language), a model-checking algorithm and a tool (AcPeg) implemented in Java. The RW formalism is for modelling access control policies. (The term `access control policy' here refers to a set of authorisation rules.) The RW language is for expressing policies modelled in the RW formalism and security properties to be verified. A property defines a goal, a coalition of agents and some conditions. A goal includes reading and overwriting certain information. Given a model built based on a policy and a property, the model-checking algorithm decides that whether the goal defined by the property is achievable by the coalition within the permissions the policy provides. The conditions defined by the property serve as pre-requirements based on which the checking is performed. In the case that the goal is achievable, the algorithm outputs strategies which may be used by the coalition to achieve the goal. The unachievability of legitimate goals may suggest that the policy does not provide the users enough permissions to carry out their actions. The achievability of malicious goals may reveal certain security holes in the policy, among which are security holes caused by 'interaction of rules', 'co-operation between agents' and 'multi-step actions'. When malicious goals are achievable, the outputting strategies help to provide clues on amending the policy. The tool implements the algorithm and thus performs the RW model-checking. -------------------------------- Date and time: Friday 30th September 2005 at 14:00 Location: UG40, School of Computer Science Title: First Things Last: Planning Proof by Induction Speaker: Jeremy Gow (http://www.uclic.ucl.ac.uk/usr/jgow/) Institution: University College London (http://www.uclic.ucl.ac.uk/) Host: Volker Sorge Abstract: A key problem in automating proof by mathematical induction is choosing an appropriate inductive inference rule. Current techniques, such as Boyer & Moore's, are either too limited or lack proper search control. I will present proof planning strategy that addresses these problems by delaying the choice of rule, and will discuss the implications it has for proof planning in general. -------------------------------- Date and time: Friday 7th October 2005 at 14:00 Location: UG40, School of Computer Science Title: An Abstract Interpretation-based Semantics for Radiation-Hard Asynchronous Circuits Speaker: Sarah Thompson (http://www.cl.cam.ac.uk/users/st326/) Institution: University of Cambridge (http://www.cl.cam.ac.uk/) Host: Aybek Mukhamedov Abstract: The effectiveness of program analysis techniques based upon sound mathematical abstract semantics has long been recognised. Though normally applied to software, this approach is also applicable to digital electronics. Most circuits are designed assuming a synchronous model; a single global clock signal drives the clock inputs of every flip flop in the system, and unclocked feedback loops are outlawed. This design approach works well, primarily because it makes circuits easy to reason about. The real world, however, is fundamentally asynchronous. Even something so simple as a push button exhibits the characteristic that it can change state at any time, requiring designers to be very careful when constructing appropriate interface circuits. Intuition based on the synchronous model tends to break down due to the need to consider timing information that is continuous in nature. Formal reasoning is generally difficult, so engineers often use inexact discrete time simulations that often miss possible pathological behaviour. Abstract interpretation provides a sound formal framework that allows abstractions of concrete systems to be reasoned about. In our SAS'04 paper, we introduced transitional logic, an abstract interpretation technique resembling a multi-valued logic that is capable of supporting reasoning about asynchronous behaviour of combinational circuits. In this talk, I will first present a gentle overview of transitional logic, then go on to show how it can be used to reason about the radiation hardness of majority voting circuits. Our analysis showed that, whilst permanent subsystem failure is tolerated as expected, brief single-event transients (SETs) of the kind typically caused by relativistic heavy ion (cosmic ray) impacts are not reliably rejected. This result can be generalised to show that, in general, delay-insensitive circuits are fundamentally incapable of rejecting SETs. This is joint work with Alan Mycroft. -------------------------------- Date and time: Friday 14th October 2005 at 14:00 Location: UG40, School of Computer Science Title: Linear Logic for the Deductive Synthesis of Grid Workflows Speaker: Lucas Dixon (http://homepages.inf.ed.ac.uk/ldixon/) Institution: University of Edinburgh (http://www.inf.ed.ac.uk/l) Host: Volker Sorge Abstract: I will describe how we are using a formalisation of intuitionistic linear logic in Isabelle, based on Abramsky's presentation [1], as a framework for deriving grid services that meet a given specification. The project is in its early stages and we describe what we believe the main challenges are and how we intend to tackle them. [1] Samson Abramsky. Computational interpretations of linear logic. Theoretical Computer Science 111(1&2):3-57, 1993 -------------------------------- Date and time: Friday 21st October 2005 at 14:00 Location: UG40, School of Computer Science Title: Partial Horn logic and cartesian theories Speaker: Steven Vickers (http://www.cs.bham.ac.uk/~sjv) Institution: The University of Birmingham (http://www.cs.bham.ac.uk) Host: Volker Sorge Abstract: Algebraic theories are a particularly simple kind of first-order logical theory, defined by sorts (we admit many-sorted theories), function symbols ("operators") and axioms in the form of universally quantified equational laws. It is well-known that these have certain good properties that are very important in universal algebra. Every algebraic theory has an initial model, got by constructing a term algebra, and then factoring out a congruence generated from the equational laws. As a corollary one can present models by the technique of generators and relations, and there are free model constructions. What is less well-known is that these properties also hold for a slightly larger class of theories, the essentially algebraic theories (Freyd) or, equivalently, cartesian theories (Coste). These use operators that are only partially defined, a paradigm example being composition of morphisms in categories. However, the formalization of these theories is a little intricate. Moreover, the use of partial operators means that the algebraic construction of initial algebras breaks down, and instead some sophisticated category theory is normally used. I shall present "partial Horn logic", a first-order logic in which function sysmbols are partial (i.e. interpreted as functions that are not everywhere defined). Unlike previous such systems, our is sequent-based, and this provides a good way to study simpler logics. It is almost identical to the framework of total logic in Johnstone's "Sketches of an Elephant" (part D1), except that equality is not reflexive (self-equality is identified with definedness) and substitution is restricted to defined terms. A minimal kind of theory in partial Horn logic is the "quasi-equational" theory. This has sorts, partial function symbols, and axioms of the sequent form phi |- psi, where the formulas phi and psi are conjunctions of equations. Quasi-equational theories are equivalent to essentially algebraic or cartesian theories. The initial model theorem holds for quasi-equational theories, and its proof is almost identical to that for algebraic theories. First form the term algebra, then factor out a *partial* congruence (not necessarily reflexive) generated from the axioms. A central step in categorical logic is the construction of classifying categories (an analogue of Lindenbaum algebras for predicate theories), and we show how these can be constructed using the initial model theorem for quasi-equational theories. This is joint work with Erik Palmgren, Dept of Mathematics, Uppsala University. -------------------------------- Date and time: Friday 4th November 2005 at 14:00 Location: UG40, School of Computer Science Title: Symbolic model-checking of dense-time systems with BDD-like data-structures Speaker: Farn Wang (http://www.iis.sinica.edu.tw/~farn/) Institution: Academia Sinica, Nankang, Taipei (http://www.iis.sinica.edu.tw/) Host: Marta Kwiatkowska Abstract: RED is a project for timed automata model-checking with BDD-like data-structures. Since its start in 1998, with the data-sharing capability of BDD-like data-structures, a series of novel techniques were developed. In this speech, we overview the following topics. . The basic theory in timed automata verification. . The basic algorithms in the symbolic model-checking of timed automata, including + weakest precondition calculation, + least fixpoint calculation, and + greatest fixpoint calculation + model-checking with multiple fairness assumptions . BDD-like data-structures for the representation and manipulations of timed automata . BDD-like data-structures for those of linear hybrid systems . Speed-up techniques for complex synchronizations and early refutations . Coverage estimation techniques for dense-time systems with BDD-like data-structures . Test case generations with state-space exploration techniques for real-time systems . Examples of using REDLIB -------------------------------- Date and time: Friday 11th November 2005 at 14:00 Location: UG40, School of Computer Science Title: Can Machines Reason like Humans in Mathematics? Speaker: Mateja Jamnik (http://www.cl.cam.ac.uk/users/mj201/) Institution: University of Cambridge (http://www.cl.cam.ac.uk/) Host: Volker Sorge, Manfred Kerber Abstract: In this talk, I present how some powerful human-oriented reasoning techniques, in particular reasoning with diagrams and learning from examples, can be modelled on machines. Human mathematicians often informally use diagrams in order to better convey solutions to problems. Yet, diagrams have only seldom been used as formal tools for reasoning - symbolic logic is the predominant method of automated reasoning. I demonstrate how formalising the use of diagrams in flexible architectures allow users (in the case of interactive systems) and systems (in the case of completely automated systems) to reason both purely diagrammatically, and with a combination of diagrammatic and symbolic inferencing methods. The second informal human reasoning technique I aim to model is the process of learning a general concept from specific examples. The rare existing research into mechanising reasoning systems that can learn from examples only addresses symbolic reasoning. The goal is to combine the use of diagrams and learning from examples by devising a system that can reason with diagrammatic, symbolic, and combined diagrammatic and symbolic methods (the so-called heterogeneous methods), and can moreover learn such methods automatically from well-chosen examples. The hope is that ultimately such a system will be able to automatically discover new, interesting and intuitive solutions to problems. -------------------------------- Date and time: Friday 18th November 2005 at 14:00 Location: UG40, School of Computer Science Title: Semantic Domains for Combining Probability and Nondeterminism:Foundations Speaker: Klaus Keimel (http://www.mathematik.tu-darmstadt.de/ags/ag14/mitglieder/keimel-de.html) Institution: Technische Universität Darmstadt, Germany (http://www.mathematik.tu-darmstadt.de/) Host: Martin Escardo Abstract: There are more and more situations where probabilistic features occur together with ordinary nondeterminism. A. McIver, C. Morgan, D. Varacca and others have considered imperative languages with probabilistic choice and purely nondeterminstic choice. They have developed a semantics for finite and discrete state spaces as well as a predicate transformer semantics. Mislove and Worrell have investigated process algebras with both probablistic and nondeterministic choice and they have developped a domain theoretical semantics for those. After motivating our approach, we will present some of the foundational work based on the thesis of R.Tix and developped further by G. Plotkin and myself. One could say that we develop tools in order to replace, e.g., finite state spaces by arbitrary continuous domains and stably compact spaces. The emphasis of the talk will be on these foundational aspects. Roughly speaking, a programme allowing probabilistic choice and nondeterministic choice starting in some initial state will be interpreted by some set of probability distributions. According to a demonic or angelic view, there will be powerdomains combining the probabilistic powerdomain with the well-known Hoare, Smyth and Plotkin powerdomains. The conceptual tools require domain theoretical analogues of probabilities and measures, topological vector spaces and Hahn-Banach type separation theorems. -------------------------------- Date and time: Friday 25th November 2005 at 14:00 Location: UG40, School of Computer Science Title: Theory and practice of theorem proving for monodic first-order temporal logic Speaker: Boris Konev (http://www.csc.liv.ac.uk/~konev/) Institution: University of Liverpool (http://www.csc.liv.ac.uk/) Host: Volker Sorge Abstract: Temporal logics have long been recognised as introducing appropriate languages for specifying a wide range of important computational properties in computer science and artificial intelligence. However, until recently, the practical use of temporal logics has largely been restricted to propositional temporal logics. First-order temporal logic has generally been avoided as no complete proof system can exist for this logic. A breakthrough by Hodkinson, Wolter, and Zakharyaschev showed that a specific fragment of first-order temporal logic, called the monodic fragment, or monodic first-order temporal logic, has the completeness property. Following the definition of the monodic fragment, the work analysing and extending this fragment has continued rapidly, and holds great promise for increasing the power of logic-based formal methods. In this talk we give an overview of a particular proof method for monodic FOTL, called monodic temporal resolution, which is based on our work on clausal temporal resolution over a number of years. The clausal resolution technique has been shown to be one of the most effective proof techniques for propositional temporal logics, and we have every reason to believe that it will be as least as successful in the case of FOTL. This calculus forms the basis of the temporal monodic theorem prover TeMP. We also consider case studies and applications. -------------------------------- Date and time: Friday 2nd December 2005 at 14:00 Location: UG40, School of Computer Science Title: Auxilliary Relations, Urysohn's Lemma and Insertion Theorems Speaker: Chris Good (http://www.mat.bham.ac.uk/C.Good/) Institution: The University of Birmingham (http://www.mat.bham.ac.uk) Host: Steven Vickers Abstract: An auxilliary relation ⊲ on a partial order ≤ is a subset of ≤ such that a) c⊲d whenever c≤a⊲b≤d and b) Interpolation: if a,b⊲c then there is some d such that a,b⊲d⊲c. Urysohn's Lemma states that a space is normal iff for any two disjoint non-empty closed sets C and D, there is a continuous real valued function taking values 0 on C and 1 on D. It is not surprising that in the poset of inclusion on subsets of a normal topological space the auxilliary relation ⊲ is closely related to Urysohn's Lemma, where A⊲B is taken to mean closure of A is a subset of B and A is a subset of interior of B. It seems that there should be a deeper connection between auxilliary relations and various topological results whose proof relies on some kind interpolation. We investigate this possibility. Joint Work With: Robin Knight (Oxford) and Ralph Kopperman (CUNY) -------------------------------- Date and time: Friday 9th December 2005 at 14:00 Location: UG40, School of Computer Science Title: Dynamics and generalization ability of Learning Vector Quantization Speaker: Michael Biehl (http://www.cs.rug.nl/~biehl/) Institution: Rijksuniversiteit Groningen, The Netherlands (http://www.rug.nl/informatica/) Host: Peter Tino Abstract: Learning schemes such as Competitive Learning and Learning Vector Quantization (LVQ) are based on the representation of data by appropriately chosen prototype vectors. While intuitively clear and widely used in a variety of classification problems, most algorithms of LVQ are heuristically motivated and lack, for instance, the relation to a well-defined cost function. Nevertheless, methods borrowed from Statistical Physics allow for a systematic study of such learning processes. Model situations in which the training is based on high-dimensional, randomized data can be studied analytically. It is possible, for instance, to compute typical learning curves, i.e. the success of learning vs. the number of example data. Besides the analysis and comparison of standard algorithms, the aim of these studies is to devise novel, more efficient training prescriptions. This talk summarizes our recent results concerning several unsupervised and supervised schemes of Vector Quantization and gives an outlook on forthcoming projects. -------------------------------- Date and time: Friday 20th January 2006 at 14:00 Location: UG40, School of Computer Science Title: A Tough Nut for Mathematical Knowledge Management Speaker: Manfred Kerber (http://www.cs.bham.ac.uk/~mmk) Institution: The University of Birmingham (http://www.cs.bham.ac.uk) Host: Volker Sorge Abstract: In this talk we address two related questions. Firstly, we want to shed light on the question how to use a representation formalism to represent a given problem. Secondly, we want to find out how different formalizations are related and in particular how it is possible to check that one formalization entails another. The latter question is a tough nut for mathematical knowledge management systems, since it amounts to the question, how a system can recognize that a solution to a problem is already available, although possibly in disguise. As our starting point we take McCarthy's 1964 mutilated checkerboard challenge problem for proof procedures and compare some of its different formalizations. -------------------------------- Date and time: Friday 3rd February 2006 at 14:00 Location: UG40, School of Computer Science Title: Resolve-Impossibility for a Contract Signing Protocol Speaker: Aybek Mukhamedov (http://www.cs.bham.ac.uk/~axm) Institution: The University of Birmingham (http://www.cs.bham.ac.uk) Host: Volker Sorge Abstract: A "pen and paper" contract signing is a traditional approach to forming a binding agreement. An electronic contract-signing protocol allows to form such agreement over a computer network. It attempts to mimic the features of "pen and paper" contract signing, especially fairness: at the end of the protocol either each signatory obtains all the other signers' contracts or no signer gets any valuable information. In "pen and paper" contract singing, fairness is generally achieved by "simultaneity", i.e. a paper contract is signed by parties at the same place and time. In an electronic contract signing, fairness is more difficult to attain, since signers are distributed and the network is asynchronous. A simple solution is to use a designated trusted party (T), who collects and then distributes all contracts. Since T may become a security and communication bottleneck, so-called "optimistic" approach has been developed. The idea is that T does not get involved, unless something goes amiss. There are essentially only two such "optimistic" contract-signing protocols proposed so far. One of them was designed by Garay and MacKenzie (Bell Labs) in 1999; it consists of a main protocol and a sub-protocol that involves a trusted party. The protocol was shown to have a flaw by Chadha, Kremer and Scedrov (Penn.State) in 2004. Those authors also presented a fix -- a revised sub-protocol for the trusted party. In this talk, I shall show that the revised protocol is also flawed for any number n>4 of signers, i.e. I shall demonstrate an attack on the protocol that breaks the fairness property. Then I will go on to argue the attack shows that the very idea behind Garay and MacKenzie's main protocol is flawed: whatever the trusted party does will result in unfairness for some signer. This means that it is impossible to define a trusted party protocol for Garay and MacKenzie's main protocol. This is a joint work with Mark Ryan. -------------------------------- Date and time: Friday 10th February 2006 at 14:00 Location: UG40, School of Computer Science Title: Qua : A generic model for categories in Linear logic, Fuzzy logic and categories of Transition systems Speaker: Priti Sinha Host: Paul Levy Abstract: A category Qua is proposed as a unification paradigm for constructions in the field of liner logic, fuzzy logic and transition systems. Many existing categories of fuzzy sets become particular cases of Qua in various ways, the category of L-fuzzy sets defined by Goguen [Goguen, 1967] is a special case of Qua. There are very intimate connections between fuzzy logic and linear logic, established by Barr [Barr, 1996] and Kreinovich, Nguyen and Wojciechowsk [KNW]. Barr has proposed the category RelL to model linear logic, it is demonstrated that RelL is an instance of Qua. Two generic constructions to produce categorical models for linear logic are , the Chu spaces, the category of games, GameK by Lafont [Lafont and Streicher, 1991] and the Dialectica categories by de Paiva [de Paiva, 1989]. These categories also emerge as special cases of Qua. The category PV defined by Blass [Blass, 1995] (which appeared explicitly in work of de Paiva on Linear Logic and in work of Vojt´aÇs on cardinal characteristic) is a special case of Qua. Also it is established that the category of transition systems with simulations as morphisms [Winskel and Nielsen, 1993] and the category of transition systems with weak form of bisimulations as morphisms form subcategories of Qua. Next an algebraic theory in Qua is constructed and further a generalization of Qua is proposed which particularizes to a category of poset-valued sets , a generic technique for building models of linear logic [Schalk and de Paiva, 2004]. -------------------------------- Date and time: Friday 17th February 2006 at 13:00 Location: LG33, Learning Center Title: A topological characterisation of Fairness Speaker: Daniele Varacca (http://www.doc.ic.ac.uk/~varacca/) Institution: Imperial College London (http://www.doc.ic.ac.uk/) Host: Paul Levy Abstract: Several computational notions have been characterised topologically. Open sets are usually seen as properties that can be observed in finite time. Closed sets represents safety properties and dense sets represent liveness properties. In this tradition we propose a topological characterisation of the notion of fairness. We propose to define fairness as co-meagerness. In this talk, I will define this topological concept and I will characterise it from a different point of view. I will show how this notion captures several different fairness notions from the literature. I will compare the topological notion with its probabilistic counterpart. Finally I will discuss how these ideas can be applied to model-checking. This is joint work with Hagen Voelzer and Ekkart Kindler. -------------------------------- Date and time: Friday 3rd March 2006 at 14:00 Location: UG40, School of Computer Science Title: A Congruence Rule Format for Name-Passing Process Calculi from Mathematical Structural Operational Semantics Speaker: Sam Staton (http://www.cl.cam.ac.uk/users/ss368/) Institution: University of Cambridge (http://www.cl.cam.ac.uk/) Host: Paul Levy Abstract: I will introduce and develop a mathematical structural operational semantics for name-passing systems, such as the pi-calculus, within Pitts' framework of nominal sets. I will explain how, from this model theory, we can extract a concrete GSOS-like rule format for name-passing process calculi for which the induced notion of behavioural equivalence --- given by a quasi-open bisimilarity --- is guaranteed to be a congruence. The presentation will involve merging several strands of research in semantics: abstract syntax, and substitution; models for process calculi with name generation; and also the mathematical structural operational semantics of Turi and Plotkin. This is joint work with Marcelo Fiore. -------------------------------- Date and time: Friday 10th March 2006 at 14:00 Location: UG40, School of Computer Science Title: Unification With Expansion Variables - a tutorial presentation Speaker: Adam Bakewell (http://cs-people.bu.edu/bake/) Institution: School of Computer Science, The University of Birmingham (http://www.cs.bham.ac.uk) Host: Dan Ghica Abstract: Unification is a fundamental technique in computer science. It has many important variants. By unification we mean finding a solution to a set of simultaneous equations of the form term1=term2. That is, a constraint set. The solution of a constraint set is usually a substitution for its variables. One solves the constraint set by applying a substitution that equates both sides of each equation. An expansion generalises the idea of a substitution. It is a special kind of term whose leaves are substitutions (rather than variables). We allow ordinary terms to contain expansion variables. This leads to a new kind of unification problem where the solution of a constraint set is an expansion that can replace term variables in the constraint with ordinary terms and expansion variables with expansions. The talk explains expansions and describes a simple rewrite system for solving constraint sets. So much for the formalities. There are many exciting aspects to this line of research. Expansion variables are a very powerful device and there are many interesting variants on the basic framework each offering new research questions. Even the simple formulation of constraint solving given in this talk is so powerful that it can simulate program evaluation (for lambda-I terms; that is, lambda terms where the 'x' of every 'lambda x.M' occurs in the 'M'.) and can be used for forms of intersection-type inference that, until recently (in type Systems 'I' and 'E'), were very difficult. -------------------------------- Date and time: Friday 17th March 2006 at 14:00 Location: UG40, School of Computer Science Title: Abstraction refinement, higher order programs and game semantics Speaker: David Lacey (http://www.dcs.warwick.ac.uk/~davel/) Institution: University of Warwick (http://www.dcs.warwick.ac.uk/) Host: Dan Ghica Abstract: In this talk I will describe a method of static analysis to check safety properties of programs. The peculiarity of the approach is that it uses game semantics as its underlying foundation and is therefore suitable for checking programs in languages including open fragments and higher-order functions. Having the semantics is one thing; having a checkable, finite (abstracted) model which can be refined to different levels of accuracy and covers all required language features is another. I will describe my progress on developing a system that uses such a model. -------------------------------- Date and time: Friday 24th March 2006 at 14:00 Location: UG40, School of Computer Science Title: Abstract Machines, Separation Logic and File Access Methods Speaker: Alan Sexton (http://www.cs.bham.ac.uk/~aps) Institution: The University of Birmingham (http://www.cs.bham.ac.uk) Host: Volker Sorge Abstract: File access methods are fundamental in data base systems, repositories and search engines. Access methods need to maintain index structures with complex data structure invariants involving pointers to pages. In recent work we have been developing an approach to specifying external (i.e. disk based) file access methods using an abstract machine based operational semantics, analysing these specifications for correctness using separation logic, and generating implementations directly from the specifications. We explain our approach and outline some of the challenges, and opportunities, posed by a number of access methods we would like to be able to deal with. This is joint work with Richard Swinbank and Hayo Thielecke -------------------------------- Date and time: Friday 31st March 2006 at 14:00 Location: UG40, School of Computer Science Title: Verification and Change-Impact Analysis of Access-Control Policies Speaker: Kathi Fisler and Shriram Krishnamurthi (http://web.cs.wpi.edu/~kfisler/) Institution: Worcester Polytechnic Institute, USA (http://web.cs.wpi.edu/) Host: Mark Ryan Abstract: Sensitive data are increasingly available on-line through the Web and other distributed protocols. System designers often create policies to capture conditions on the access to data. To reduce source clutter and improve maintenance, developers increasingly use domain-specific, declarative languages to express these policies. In turn, administrators need to analyze policies relative to properties, and to understand the effect of policy changes even in the absence of properties. This talk discusses models and techniques that support both kinds of analyses for role-based access-control policies. It discusses Margrave, a software tool that implements these analyses for standalone policies, and discusses work in progress on models that also account for the dynamic environment in which policies execute. This extension enables reasoning about interactions between policies and the programs that employ them, but using analyses that extend beyond conventional model checking. This is joint work with Dan Dougherty. -------------------------------- Date and time: Friday 19th May 2006 at 14:00 Location: UG40, School of Computer Science Title: Proof Presentation Speaker: Jörg Siekmann (http://www-ags.dfki.uni-sb.de/home1.html) Institution: Universität des Saarlandes and DFKI Saarbrücken, Germany (http://www.dfki.de) Host: Manfred Kerber Abstract: The talk is based on a book about the human-oriented presentation of a mathematical proof in natural language, in a style as we may find it in a typical mathematical text book. How can a proof be other than human-oriented? What we have in mind is a deduction system, which is implemented on a computer, that proves — with some human interaction — a mathematical textbook as may be used in an undergraduate course. The proofs generated by these systems today are far from being human-oriented and can in general only be read by an expert in the respective field: proofs between several hundred (for a common mathematical theorem), for more than a thousand steps (for an unusually difficult theorem) and more than ten thousand deduction steps (in a program verification task) are not uncommon. Although these proofs are provably correct,they are typically marred by many problems: to start with, that are usually written in a highly specialised logic such as the resolution calculus, in a matrix format, or even worse, they may be generated by a model checker. Moreover they record every logical step that may be necessary for the minute detail of some term transformation (such as, for example, the rearrangement of brackets) alongside with those arguments, a mathematician would call important steps or "heureka"-steps that capture the main idea of the proof. Only these would he be willing to communicate to his fellow mathematicians—provided they have a similar academic background and work in the same mathematical discipline. If not, i.e. if the proof was written say for an undergraduate textbook, the option of an important step may be viewed differently depending on the intended reader. Now, even if we were able to isolate the ten important steps — out of those hundreds of machine generated proof steps — there would still be the startling problem that they are usually written in the ‘wrong’ order. A human reader might say: ‘they do not have a logical structure’; which is to say that of course they follow a logical pattern (as they are correctly generated by a machine), but, given the convention of the respective field and the way the trained mathematician in this field is used to communicate, they are somewhat strange and ill structured. And finally, there is the problem that proofs are purely formal and recorded in a predicate logic that is very far from the usual presentation that relies on a mixture of natural language arguments interspersed with some formalism. The book ( about 800 page) which gives an answer to some of these problems is to appear with Elsevier -------------------------------- Date and time: Friday 9th June 2006 at 14:00 Location: UG40, School of Computer Science Title: Extended Directed Search for Probabilistic Timed Reachability Speaker: Husain Aljazzar (http://www.inf.uni-konstanz.de/~aljazzar/) Institution: Universität Konstanz, Germany (http://www.inf.uni-konstanz.de) Host: Marta Kwiatkowska Abstract: Currently, stochastic model checkers can efficiently analyse stochastic models. However, they are unable to provide debugging information in the form of offending system traces, in model checking parlance commonly referred to as counterexamples. This constrains the practical use of stochastic model checking. In this talk I will present our method to select counterexamples for probabilistic timed reachability properties on discrete-time and continuous-time Markov chains. For the diagnostics of probabilistic reachability it is usually inevitable to consider sets of failure traces. For a given probabilistic timed reachability property, we employ extended directed explicit-state search algorithms based on BF and Z$^*$ to determine a subgraph of the model's state transition graph inducing a set of failure traces which carries a large proportion of probability mass. For this purpose we introduce a probabilistic evaluation function to measure the quality of failure traces. Such failure subgraphs are not just essential tools for diagnostics but, in particular cases, they also provide real counterexamples which can be used to show the violation of the given property. They also allow the solution of timed probabilistic reachability properties to be approximated from below. In this talk, I am going to give an overview of the approach and to illustrate it using some case studies. -------------------------------- Date and time: Friday 23rd June 2006 at 14:00 Location: UG40, School of Computer Science Title: Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic Speaker: Hongseok Yang (http://ropas.snu.ac.kr/~hyang/) Institution: Seoul National University, Korea (http://ropas.snu.ac.kr) Host: Uday Reddy Abstract: Previous shape analysis algorithms assume that the heap can be characterized in terms of reachability, that it is composed of discrete nodes that can be accessed only via access paths built from variables and field names. This assumption is violated by pointer arithmetic. In this talk I will describe a shape analysis that works in the presence of pointer arithmetic. The abstract domain uses formulae in separation logic, leveraging that logic's non-reliance on reachability assumptions for its soundness. The analysis has been applied to verify series of programs for dynamic memory management. This is joint work with Dino Distefano, Peter O'Hearn and Cristiano Calcagno. -------------------------------- Date and time: Friday 30th June 2006 at 14:00 Location: UG40, School of Computer Science Title: Bidomains and Full Abstraction for Countable Nondeterminism Speaker: Jim Laird (http://www.cogs.susx.ac.uk/users/jiml/) Institution: University of Sussex (http://www.cogs.susx.ac.uk/) Host: Dan Ghica Abstract: We describe a denotational semantics for a sequential functional language with random number generation over the natural numbers, and prove that it is fully abstract with respect to may-and-must testing. Our model is based on biordered sets similar to Berry's bidomains, and stable, monotone functions. However, (as in prior models of unbounded non-determinism) these functions may not be continuous. Working in a biordered setting allows us to exploit the different properties of both extensional and stable orders to construct a Cartesian closed category of sequential, discontinuous functions, with least and greatest fixpoints having strong enough properties to prove computational adequacy. We establish full abstraction of the semantics by showing that it contains a simple, first-order ``universal type-object'' within which all types may be embedded using functions defined by (countable) ordinal induction. -------------------------------- Date and time: Monday 17th July 2006 at 16:00 Location: UG40, School of Computer Science Title: Structured strategies for games on finite graphs Speaker: Sunil Easaw Simon (http://www.imsc.res.in/tcsweb/students/sunils.html) Institution: Institute of Mathematical Sciences, Chennai, India (http://www.imsc.res.in/) Host: Uday Reddy Abstract: We consider infinite plays over finite game graphs where players have possibly overlapping objectives. When strategies are functions that map game positions or plays to moves, existence of bounded memory best response strategies can be established. However, when an opponent's strategy is known only by its properties, the notion of best response needs to be re-examined. We propose a structural definition of strategies built up from atomic decisions of the form ``when condition x holds play a'' and where a player's strategy may depend on properties of other players' strategies. These strategies can be represented by finite state automata. In this framework, we look at the algorithmic questions of checking whether a strategy achieves a certain objective and synthesising strategies to achieve certain conditions. We propose a simple logic to describe composite strategies and reason about how they ensure players' objectives. We show that checking such an assertion on a game graph is decidable. We also present an axiom system for the logic and prove that it is complete. This is joint work with R. Ramanujam(IMSc). -------------------------------- Date and time: Tuesday 18th July 2006 at 16:00 Location: UG40, School of Computer Science Title: Synthesis from Temporal Specifications Speaker: Nir Piterman (http://mtc.epfl.ch/~piterman/) Institution: EPFL, Lausanne, Switzerland (http://mtc.epfl.ch/) Host: Marta Kwiatkowska Abstract: One of the most ambitious goals in the field of verification is to automatically produce designs from their specifications, a process called {em synthesis}. We are interested in {em reactive systems}, systems that continuously interact with other programs, users, or their environment (like operating systems or CPUs). The complexity of reactive system does not necessarily arise from computing complicated functions but rather from the fact that they have to be able to react to all possible inputs and maintain their behavior forever. The most appropriate way to consider synthesis is by considering two-sided games between the system and the environment. The environment tries to falsify the specification and the system tries to satisfy it. Every system move (the way the system handles its internal variables) has to match all possible future moves of the environment. The system wins the game if it has a strategy such that all infinite traces satisfy the specification. When the specification is a {em linear temporal logic} formula or a {em nondeterministic B`uchi automaton}, the problem is reduced to solving simpler games by constructing deterministic automata. However, determinization for automata on infinite words is extremely complicated. Here we show how to construct nondeterministic automata that can replace deterministic automata in the context of games and synthesis. The fact that our automata are nondeterministic makes them surprisingly simple, amenable to symbolic implementation, and allows a natural hierarchy of automata of increasing complexity that lead to the full solution. -------------------------------- Date and time: Friday 1st September 2006 at 14:00 Location: UG40, School of Computer Science Title: Combining Model Checking and Proof for Probabilistic systems Speaker: Annabelle McIver (http://www.ics.mq.edu.au/gen/person/anabel.html) Institution: Macquarie University, Australia (http://www.ics.mq.edu.au/) Host: Marta Kwiatkowska Abstract: The combination of standard model checking techniques with proof-based techniques has successfully been applied to verification in such a way that the strength of each method complements the other. Thus the combined approach is better than either one alone. In this talk we shall explore the extent to which the combination can be achieved in probabilistic model checking. -------------------------------- Date and time: Monday 4th September 2006 at 13:00 Location: UG40, School of Computer Science Title: Analysis of Recursive Markov Chains, Recursive Markov Decision Processes, and Recursive Stochastic Games. Speaker: Kousha Etessami (http://homepages.inf.ed.ac.uk/kousha/) Institution: University of Edinburgh (http://www.inf.ed.ac.uk) Host: Marta Kwiatkowska Abstract: Recursive Markov Chains (RMCs) are a natural abstract model of procedural probabilistic programs and other systems involving both recursion and probability. RMCs define a class of denumerable Markov chains with a rich theory generalizing that of multi-type Branching Processes and Stochastic Context-Free Grammars, and they are tightly related to probabilistic Pushdown Systems. Recursive Markov Decision Processes (RMDPs) and Recursive Stochastic Games (RSGs) extend RMCs with a controller and two adversarial players, respectively. In a series of recent papers we have studied central algorithmic analysis and verification questions for RMCs, RMDPs, and RSGs, providing some strong upper and lower bounds on the complexity of key algorithmic problems. I will provide a broad survey of this work, indicate some of the main techniques involved in our analyses, discuss potential application domains, and indicate some of the many directions for future research. This talk surveys joint work with Mihalis Yannakakis (Columbia U.) contained in a series of recent papers that appear at: STACS'05, TACAS'05, ICALP'05, QEST'05, STACS'06, and ICALP'06. -------------------------------- Date and time: Friday 29th September 2006 at 14:00 Location: UG40, School of Computer Science Title: Geometry of Synthesis: A structural approach to VLSI design Speaker: Dan Ghica (http://www.cs.bham.ac.uk/~drg) Institution: School of Computer Science (http://www.cs.bham.ac.uk) Host: N/A Abstract: We propose a new technique for hardware synthesis from higher-order functional languages with imperative features, based on Reynolds's "Syntactic Control of Interference". The restriction on contraction in the type system is useful to manage the difficult issue of sharing of physical circuits. We use a semantic model inspired by game semantics and the geometry of interaction, and express it directly as a certain class of digital circuits that form a cartesian, monoidal-closed category. A soundness result is given, which is also a correctness result for the compilation technique. Concurrency and recursion raise some difficult issues that are highlighted, along with potential approaches to a solution. A proof-of-concept compiler from SCI to Verilog (a hardware specification language) will be discussed. -------------------------------- Date and time: Thursday 5th October 2006 at 16:00 Location: UG40, School of Computer Science Title: Relational Parametricity for Computational Effects Speaker: Alex Simpson (http://homepages.inf.ed.ac.uk/als/) Institution: University of Edinburgh (http://www.inf.ed.ac.uk) Host: Martin Escardo Abstract: According to Strachey, a polymorphic program is parametric if it applies a uniform algorithm independently of the type instantiations at which it is applied. The notion of relational parametricity, introduced by Reynolds, is one possible mathematical formulation of this idea. Relational parametricity provides a powerful tool for establishing data abstraction properties, proving equivalences of datatypes, and establishing equalities of programs. Such properties have been well studied in a pure functional setting. Real programs, however, exhibit computational effects. In this paper, we develop a framework for extending the notion of relational parametricity to languages with effects. -------------------------------- Date and time: Friday 13th October 2006 at 14:00 Location: UG40, School of Computer Science Title: Concurrent Separation Logic: a message from the front line Speaker: Matthew Parkinson (http://www.cl.cam.ac.uk/~mjp41/) Institution: University of Cambridge (http://www.cl.cam.ac.uk/) Host: Hayo Thielecke Abstract: In this talk I will present two areas that I have been extending separation logic in: (1) using * to separate stack variables; and (2) verifying non-blocking algorithms. (1) Normally in separation logic * separates the heap, and we inherit the side-conditions of standard Hoare logic to deal with the program variables. However, in the concurrent setting these side-conditions are overly restrictive and prevent us verifying many safe programs. By extending the logic to use * to separate variables, we can soundly remove the side-conditions and verify a wider class of programs. (2) O'Hearn has shown concurrent separation logic can reason elegantly about blocking concurrency. I will show how this same reasoning can be applied to non-blocking concurrency, and discuss an example of Maged Michael's non-blocking stack using Hazard pointers. -------------------------------- Date and time: Friday 27th October 2006 at 14:00 Location: UG40, School of Computer Science Title: Quasi-Linear Types for Mutable Data Structures Speaker: Alan Mycroft (http://www.cl.cam.ac.uk/~am21/) Institution: University of Cambridge (http://www.cl.cam.ac.uk) Host: Uday Reddy Abstract: The specification of an abstract data type may admit several different implementations, some of which may exploit mutability and hence have subtle safety contracts that are expressed only informally or not at all. We address the problem of specifying interface types for mutable data structures which constrain usage of their operations to conform to their corresponding (functional) algebraic data type specifications. Focussing on the stack ADT, we first explore two distinct mutable implementations and use a new variant of quasi-linear types to define interfaces which restrict the use of their operations to conform to the functional norm. In doing so we reconcile the abstract specifications of data types with their real-world implementations. The second half of the paper applies these techniques to the implementation of structural operational semantics by considering the formal stepwise development (within SOS) of the traditional ``stack and free-variable list'' implementation of an ML-like language from a conventional explicit substitution model. -------------------------------- Date and time: Friday 3rd November 2006 at 14:00 Location: UG40, School of Computer Science Title: On Repairing Reasoning Reversals via Representational Refinements Speaker: Alan Bundy (http://homepages.inf.ed.ac.uk/bundy/) Institution: University of Edinburgh (http://www.inf.ed.ac.uk/) Host: Volker Sorge Abstract: Representation is a fluent. A mismatch between the real world and an agent's representation of it can be signalled by unexpected failures (or successes) of the agent's reasoning. The 'real world' may include the ontologies of other agents. Such mismatches can be repaired by refining or abstracting an agent's ontology. These refinements or abstractions may not be limited to changes of belief, but may also change the signature of the agent's ontology. We describe the implementation and successful evaluation of these ideas in the ORS system. ORS diagnoses failures in plan execution and then repairs the faulty ontologies. Our automated approach to dynamic ontology repair has been designed specifically to address real issues in multi-agent systems, for instance, as envisaged in the Semantic Web. -------------------------------- Date and time: Friday 10th November 2006 at 14:00 Location: UG40, School of Computer Science Title: DEEP INFERENCE, PROOF COMPLEXITY AND PROOF IDENTITY Speaker: Alessio Guglielmi (http://alessio.guglielmi.name/res/index.html) Institution: University of Bath (http://www.bath.ac.uk/comp-sci/) Host: Achim Jung Abstract: Deep inference is a new methodology in proof theory. In deep inference, we can design deductive systems whose inference rules operate on minimal amounts of information with extreme freedom. This way, we can overcome many difficulties of formalisms like the sequent calculus and natural deduction. In this introductory talk, I will show how to use deep inference for getting exponential speed-ups in proof complexity. I will also show how cut elimination in deep inference can be achieved, so making for a reasonable proof theory. Before getting into these details, I will motivate deep inference as a way of approaching the problem of proof identity, and, more in general, proof semantics. This talk will not require any specialised knowledge of proof theory, proof complexity and proof semantics. More information on deep inference is at . -------------------------------- Date and time: Friday 17th November 2006 at 14:00 Location: UG40, School of Computer Science Title: Full Completeness Revisited Speaker: Samson Abramsky (http://web.comlab.ox.ac.uk/oucl/people/samson.abramsky.html) Institution: Oxford University Computing Laboratory (http://web.comlab.ox.ac.uk/) Host: Uday Reddy Abstract: We pursue the program of exposing the intrinsic mathematical structure of the ``space of proofs'' of a logical system. We study the case of Multiplicative-Additive Linear Logic (MALL). We use tools from Domain theory to develop a semantic notion of proof net for MALL. We also give an interactive criterion for strategies, formalized in the same Domain-theoretic setting, to come from proofs, and show that a ``semantic proof structure'' satisfies the geometric correctness criterion for proof-nets if and only if it satisfies the interactive criterion for strategies. We can also use the Domain-theoretic setting to give an elegant compositional account of Cut-Elimination. This work is a continuation of previous joint work with Radha Jagadeesan and Paul-Andre Mellies. -------------------------------- Date and time: Friday 24th November 2006 at 14:00 Location: UG40, School of Computer Science Title: When While is a Security Risk Speaker: Pasquale Malacaria (http://www.dcs.qmul.ac.uk/~pm/) Institution: Queen Mary University of London (http://www.dcs.qmul.ac.uk) Host: Dan Ghica Abstract: There is a clear intuitive connection between the notion of leakage of information in a program and concepts from information theory. This intuition has not been satisfactorily pinned down, until now. In particular, previous information-theoretic models of programs are imprecise, due to their overly conservative treatment of looping constructs. We present the first precise information-theoretic semantics of looping constructs. Our semantics describes both the amount and rate of leakage; if either is small enough, then a program might be deemed "secure''. Using the semantics we provide an investigation and classification of bounded and unbounded covert channels. -------------------------------- Date and time: Friday 1st December 2006 at 14:00 Location: UG40, School of Computer Science Title: Automatic termination proofs for software Speaker: Byron Cook (http://research.microsoft.com/~bycook/) Institution: Microsoft Research, Cambridge (http://research.microsoft.com/) Host: Dan Ghica Abstract: I will describe recent advances in the area of automatic program termination analysis. In particular, I will describe the development of several automatic tools, called TERMINATOR and MUTANT , which implement new termination analysis algorithms. These tools have been used to prove that Windows device driver dispatch routines always return control back to their caller. The tools have also found a number of critical termination bugs in device drivers. -------------------------------- Date and time: Friday 8th December 2006 at 14:00 Location: UG40, School of Computer Science Title: Generative Unbinding of Names Speaker: Andrew Pitts (http://www.cl.cam.ac.uk/~amp12/) Institution: University of Cambridge Computer Laboratory (http://www.cl.cam.ac.uk) Host: Dan Ghica Abstract: In this talk I will discuss what operations on names can co-exist with a programming language construct for name binding that enforces alpha-equivalence via a type system. The particular form of typed name binding I consider is that used by the FreshML family of languages. Its characteristic feature is that a name binding is represented by an abstract (name,value)-pair that may only be deconstructed via the generation of fresh bound names. In FreshML the only observation one can make of names is to test whether or not they are equal. This restricted amount of observation was thought necessary to ensure that there is no observable difference between alpha-equivalent name binders. Yet from an algorithmic point of view it would be desirable to allow other operations and relations on names, such as a total ordering. It turns out that, contrary to expectations, one may add not just ordering, but almost any relation or numerical function on names without disturbing the fundamental correctness result about this form of name binding (that object-level alpha-equivalence precisely corresponds to contextual equivalence at the programming meta-level), so long as one takes the state of dynamically created names into account. -------------------------------- Date and time: Friday 15th December 2006 at 14:00 Location: UG40, School of Computer Science Title: Interaction and Depth against Nondeterminism in Proof Search Speaker: Ozan Kahramanogullari (http://www.doc.ic.ac.uk/~ozank/) Institution: Imperial College London (http://www.doc.ic.ac.uk/) Host: Achim Jung Abstract: Deep inference is a proof theoretic methodolgy for designing deductive systems. In deep inference, in contrast to the sequent calculus inference rules, inference rules can be applied at any depth inside formulae. Unlike the sequent calculus presentations, deep inference presentation of classical logic polynomially simulates popular proof procedures such as resolution. However, applicability of the inference rules at any depth causes greater nondeterminism than in the sequent calculus regarding proof search. Although deep inference provides much shorter proofs than, for example, in the sequent calculus, this wild nondeterminism is a drawback for applications. In this talk, I am going to discuss the proof theory of a technique for reducing nondeterminism in deep inference systems. By means of conditions that exploit an interaction schema on the formulae, this technique allows to redesign the inference rules in such a way that reduces nondeterminism without losing the shorter proofs. However, when these interaction rules are applied during proof search to formulae of arbitrary size, performing the check of the condition of the interaction rules becomes computationally expensive. In the second part of this talk, I will discuss the proof theory of deep inference systems where inference rules are allowed only at the `deepest´ positions. Because deepest instances of the inference rules are applied on the smaller subformulae, the check of the condition of the interaction rules is performed only on these smaller formulae. -------------------------------- Date and time: Friday 19th January 2007 at 14:00 Location: UG40, School of Computer Science Title: On the ubiquity of certain total type structures Speaker: John Longley (http://homepages.inf.ed.ac.uk/jrl/) Institution: University of Edinburgh (http://homepages.inf.ed.ac.uk/) Host: Martin Escardo Abstract: It is a fact of experience from the study of higher type computability that a wide range of approaches to defining a class of (hereditarily) total functionals over N leads in practice to a relatively small handful of distinct type structures. Among these are the type structure C of Kleene-Kreisel continuous functionals, its effective substructure C^eff, and the type structure HEO of the hereditarily effective operations. However, the proofs of the relevant equivalences are often non-trivial, and it is not immediately clear why these particular type structures should arise so ubiquitously. In this talk we present some new results which go some way towards explaining this phenomenon. Our results show that a large class of extensional collapse constructions always give rise to C, C^eff or HEO (as appropriate). We obtain versions of our results for both the ``standard'' and ``modified'' extensional collapse constructions. The proofs make essential use of a technique due to Normann. Many new results, as well as some previously known ones, can be obtained as instances of our theorems, but more importantly, the proofs apply uniformly to a whole family of constructions, and provide strong evidence that the above three type structures are highly canonical mathematical objects. -------------------------------- Date and time: Friday 26th January 2007 at 14:00 Location: UG40, School of Computer Science Title: A Unified Category-Theoretic Semantics for Binding Signatures in Substructural Logics Speaker: John Power (http://www.inf.ed.ac.uk/people/staff/John_Power.html) Institution: University of Edinburgh (http://www.inf.ed.ac.uk/) Host: Paul Levy Abstract: Generalising Fiore et al's use of the category FF of finite sets to model untyped cartesian contexts and Tanaka's use of the category PP of permutations to model untyped linear contexts, we let S be an arbitrary pseudo-monad on Cat and let S1 model untyped contexts in general: this generality includes contexts for sub-structural logics such as the Logic of Bunched Implications and variants. Given a pseudo-distributive law of S over the (partial) pseudo-monad for free cocompletions, we define a canonical substitution monoidal structure on the category [(S1)^{op},Set], generalising substitution monoidal structures for cartesian and linear contexts and providing a natural substitution structure for Bunched Implications and its variants. We give a concrete description of the substitution monoidal structure. We then give an axiomatic definition of a binding signature, again extending the definitions for cartesian and linear contexts. We investigate examples in detail, then prove the central result of the paper, yielding initial algebra semantics for binding signatures at the level of generality we propose. -------------------------------- Date and time: Friday 2nd February 2007 at 14:00 Location: UG40, School of Computer Science Title: Quadrality Speaker: Paul Taylor Host: Martin Escardo Abstract: Quadrality is a square of adjunctions that combines the traditional dual equivalence of linear algebra and linear logic with Girard's decomposition of function-spaces in domain theory and Abstract Stone Duality. I shall how this applies to set theory, order theory and two examples in domain theory, though the idea ought also to be applicable in commutative algebra. Finally I shall sketch the strategy for trying to use it to construct a supercategory for topology. -------------------------------- Date and time: Friday 9th February 2007 at 14:00 Location: UG40, School of Computer Science Title: Lava: Optimizing Circuit Layout for FPGAs Speaker: Satnam Singh (http://research.microsoft.com/~satnams/) Institution: Microsoft Research (http://research.microsoft.com/) Host: Dan Ghica Abstract: This presentation provides an introduction to the Lava system for compact and efficient structural circuit design for FPGAs. The Lava system is a collection of Haskell libraries which specifies a domain specific language for composing the interconnection and layout of gates. The system makes extensive use of higher order combinators to specify combinators that can generate new composite circuits in a way which that not possible with conventional languages like VHDL and Verilog. We give an example of a high speed sorter circuit based on Batcher's bitonic merger (and hopefully hardware demo). Finally, we show how close one can encode a Lava-like language in an imperative language like C# which now has limited support for lambda expressions ("delegates"). -------------------------------- Date and time: Friday 23rd February 2007 at 14:00 Location: UG40, School of Computer Science Title: Self-similarity and recursion Speaker: Tom Leinster (http://www.maths.gla.ac.uk/~tl/) Institution: University of Glasgow (http://www.maths.gla.ac.uk/~tl/) Host: Dan Ghica Abstract: A common situation in mathematics and computer science is that we have a family of objects, each one described in terms of the others. A simple example is a system of simultaneous linear equations in which each of the variables involved appears as the left-hand side of exactly one of the equations. Similarly, we might have a famly of datatypes defined in a mutually recursive way. It turns out that there is a useful general theory of such situations, connecting (among other things) to self-similarity in the world of topology. I will explain some of this theory and what it might be good for. -------------------------------- Date and time: Friday 2nd March 2007 at 14:00 Location: UG40, School of Computer Science Title: Profinite Heyting algebras Speaker: Nick Bezhanishvili (http://www.cs.le.ac.uk/people/nb118/) Institution: University of Leicester (http://www.cs.le.ac.uk/) Abstract: An algebra A in a variety V is called profinite if A is an inverse limit of finite V-algebras. In this talk, I will give a complete characterization of profinite Heyting algebras. This result implies a well-known description of profinite Boolean algebras and distributive lattices. -------------------------------- Date and time: Tuesday 6th March 2007 at 11:00 Location: Room 245, School of Computer Science Title: Relational Parametricity for Control Considered as a Computational Effect Speaker: Rasmus Mogelberg (http://www.lfcs.inf.ed.ac.uk/people/profiles/Rasmus_Mogelberg.html) Institution: University of Edinburgh (http://www.lfcs.inf.ed.ac.uk/) Host: Paul Levy Abstract: This paper investigates parametric polymorphism in the presence of control operators. Our approach is to specialise a general type theory combining polymorphism and computational effects, by extending it with additional constants expressing control. By defining relationally parametric models of this extended calculus, we capture the interaction between parametricity and control. As a worked example, we show that recent results of M. Hasegawa on type definability in the second-order (call-by-name) lambda-mu-calculus arise as special cases of general results valid for arbitrary computational effects. -------------------------------- Date and time: Thursday 15th March 2007 at 13:00 Location: LG52, Learning Centre Title: The Locale of Random Sequences Speaker: Alex Simpson Institution: University of Edinburgh Host: Martin Escardo Abstract: If one tosses a fair coin ad infinitum one generates a "random sequence" in {0,1}^omega. According to probability theory, such a sequence will "almost surely" satisfy the familiar probabilistic laws: law of large numbers, law of the iterated logarithm, etc. As is well known, the measure-theoretic quantification of "almost surely" is necessary here, because there are no sequences at all that satisfy *all* probabilistic laws simultaneously. In this talk I will show that there is nonetheless a natural and meaningful "space" of sequences that do satisfy all probabilistic laws. The tool needed to make sense of this idea is locale theory. The aim of the talk is to present sufficient background on randomness and locale theory to lead up to the eventual very natural definition of the "locale of random sequences". Finally, I'll discuss some interesting properties of this "space". The following brainteaser (adapted from an example of van Lambalgen) may help motivate the context for the talk. A casino runs a new game. Each day it takes bets on the outcome of a coin toss. If the result of the toss on that day is 0 then all punters win, and they win the amount that they bet. If, however, the result is 1 then then casino wins and takes all the money bet. As casino games go, this appears to be a particularly fair one for punters, since there is zero expected loss per toss. However, the management of the casino is corrupt, and intends to make its money by cheating. Instead of tossing a fair coin, on day n, the casino tosses a coin whose probability of coming up 1 is 0.5 + delta_n. What the casino wants to do is to disguise the fact that it is cheating by choosing values delta_n > 0 in a sufficiently clever way that the sequence it generates is indistinguishable from a genuine fair random sequence. QUESTION 1 Is is possible for the casino to cheat the customer in this way without its deception being detectable? QUESTION 2 If so, what are the constraints on the sequence (delta_n)? QUESTION 3 If such a game is possible, can the casino use it to make unlimited profits? There is also a more fundamental meta-question: QUESTION 4 How does one make mathematical sense of the informal questions above? -------------------------------- Date and time: Friday 16th March 2007 at 14:00 Location: UG40, School of Computer Science Title: HD-automata with distinctions Speaker: Emilio Tuosto (http://www.cs.le.ac.uk/people/et52/) Institution: University of Leicester (http://www.cs.le.ac.uk/) Host: Paul Levy Abstract: History Dependent automata (HDA) provides syntax-independentoperational models of a class of history-dependent formalisms. States and transitions of HDA are enriched with (finite sets of) names and symmetries on them. Previously, HDA have been successfully applied formodelling early and late bisimulation in pi-calculus and hyperbisimulation in Fusion calculus. However, current HDA are not adequate for modelling behavioural semantics where more sophisticated forms of name relationships are central. An example of such semantics is the open bisimulation of the pi-calculus, modelled by Sangiorgi by means of a symbolic semantics exploiting distinctions for controlling name instantiations. In fact, the open bisimulation is closed under all substitution respecting name distinctions. In this paper we tackle the problem by introducing a category of HDA built on top of named sets with distinctions. Specifically, we extend named sets, the basic building blocks of HDA, with a notion of distinction so that names can coalesce if the distinction allows to. As a case study, we show how HDA over named sets with distinctions can model open bisimulation of pi-calculus. -------------------------------- Date and time: Friday 23rd March 2007 at 14:00 Location: UG40, School of Computer Science Title: Automated verification of probabilistic programs Speaker: Andrzej Murawski (http://web.comlab.ox.ac.uk/oucl/work/andrzej.murawski/index.html) Institution: Oxford University Computing Laboratory (http://web.comlab.ox.ac.uk/) Host: Dan Ghica Abstract: We present APEX, a verification tool for probabilistic systems, which takes as input programs written in a C/Pascal-like programming language. Unlike other probabilistic model-checkers, APEX is based on game semantics and can accommodate high-level programming idioms such as procedures and arrays. We illustrate our approach with three non-trivial case studies: Herman's self-stabilisation algorithm, an analysis of the shapes of trees obtained by certain sequences of random insertions and deletions, and the question of anonymity in the dining cryptographers protocol. This is joint work with A. Legay, J. Ouaknine and J. Worrell. -------------------------------- Date and time: Friday 30th March 2007 at 14:00 Location: UG40, School of Computer Science Title: Local Reasoning about Higher-Order Store Speaker: Bernhard Reus Institution: University of Sussex Host: Hayo Thielecke Abstract: Separation Logic is a sub-structural logic that supports local reasoning for imperative programs with dynamic memory. It was designed to elegantly describe sharing and aliasing properties of heap structures, thus facilitating the verification of programs with pointers. Various flavours of separation logic have been developed for heaps containing records of basic data types. Languages like C or ML, however, also allow procedures to be stored on the heap, giving rise to code pointers. Such type of heap is often referred to as "higher-order store." -------------------------------- Date and time: Friday 4th May 2007 at 14:00 Location: UG40, School of Computer Science Title: Full Abstraction for Nominal General References Speaker: Nikos Tzevelekos Institution: Oxford University Abstract: Game semantics has been used with considerable success in formulating fully abstract semantics for languages with higher-order procedures and a wide range of computational effects. Recently, nominal games have been proposed for modeling functional languages with names. These are ordinary games cast in the theory of nominal sets developed by Pitts and Gabbay. Here we take nominal games one step further, by developing a fully abstract semantics for a language with nominal general references. -------------------------------- Date and time: Friday 25th May 2007 at 14:00 Location: UG40, School of Computer Science Title: Drivers, choreography, planning and the Dialectica Interpretation: a whistlestop tour of some of the theoretical research at Queen Mary Speaker: Edmund Robinson Institution: Queen Mary University of London Host: Achim Jung Abstract: Since much of my own recent work has been with Eike Ritter, I am giving a whistestop tour through some of the other research going on in the Theory group at Queen Mary. An underlying theme is theory reaching out in some non-obvious directions. These range from the work of Peter O'Hearn's group with Microsoft on driver verification, through Kohei Honda's with W3C on web service choreography, Max Kanovich's on the benefits of linear logic for planning, and Paulo Oliva's on a common framework for the Dialectica Interpretation and Kleene's modified realizability. Not to mention Pasquale Malacaria's work on information leakage and (separately) the Adaboost algorithm. -------------------------------- Date and time: Friday 1st June 2007 at 14:00 Location: UG40, School of Computer Science Title: TBA Speaker: Anton Setzer Institution: University of Swansea Host: Achim Jung, Eike Ritter -------------------------------- Date and time: Friday 22nd June 2007 at 14:00 Location: UG40, School of Computer Science Title: TBA Speaker: Sergio Maffeis Institution: Imperial College Host: Achim Jung -------------------------------- Date and time: Friday 24th August 2007 at 14:00 Location: UG40, School of Computer Science Title: Recent case studies in proof mining Speaker: Paulo Oliva Institution: Queen Mary University of London Host: Martin Escardo Abstract: Proof mining is the branch of proof theory concerned with extracting new quantitative (e.g. bounds) and qualitative (i.e. new results) information from (ineffective) proof in arithmetic and analysis. The main proof theoretic technique used is functional interpretation. In this talk I plan to first describe the technique and show how it applies to simple examples. Then I will survey the most recent case studies in fixed point theory [Kohlenbach/Leustean] and ergodic theory [Avigad/Gerhardy]. -------------------------------- Date and time: Friday 14th September 2007 at 14:00 Location: UG40, School of Computer Science Title: Baltic: Service Combinators for Farming Virtual Machines Speaker: Andy Gordon Institution: Microsoft Research, Cambridge Host: Mark Ryan Abstract: We consider the problem of managing server farms largely automatically, in software. Automated management is gaining in importance with the widespread adoption of virtualization technologies, which allow multiple virtual machines per physical host. We consider the case where each server is service-oriented, in the sense that the services it provides, and the external services it depends upon, are explicitly described in metadata. We describe the design, implementation, and formal semantics of a library of combinators whose types record and respect server metadata. Our implementation consists of a typed functional script built with our combinators, in control of a Virtual Machine Monitor hosting a set of virtual machines. Our combinators support a range of operations including creation of virtual machines, their interconnection using typed endpoints, and the creation of intermediaries for tasks such as load balancing. Our combinators also allow provision and reconfiguration in response to events such as machine failures or spikes in demand. We describe a series of programming examples run on our implementation, based on existing server code for order processing, a typical data centre workload. To obtain a formal semantics for any script using our combinators, we provide an alternative implementation of our interface using a small concurrency library. Hence, the behaviour of the script plus our libraries can be interpreted within a statically typed process calculus. Assuming that server metadata is correct, a benefit of typing is that various server configuration errors are detected statically, rather than sometime during the execution of the script. -------------------------------- Date and time: Friday 28th September 2007 at 14:00 Location: UG40, School of Computer Science Title: Solving functional equations reliably with arbitrary precision Speaker: Michal Konecny Institution: Aston University Abstract: I will describe a graphical language to express higher-order numeric equations such as differential equations. The denotational semantics of the language is similar to the semantics of Kahn networks, except that the data items that `flow' through channels are differentiable functions or functionals. I will show how several well-known differential equations can be expressed in this way and how one can give operational semantics to the language to obtain a converging sequence of enclosures to the exact solutions of such equations with a reasonable efficiency. The main issues with this approach are: mode of communication between nodes, representations of differentiable functions and functionals, avoiding fixed-points with little information and analysing the speed of convergence. I will relate my proposal both to classical numerical methods and to other frameworks for reliable arbitrary precision computation. The leading example is an adaptive and parallelised version of the Initial Value Problem solving algorithm by Edalat and Pattinson. -------------------------------- Date and time: Friday 5th October 2007 at 14:00 Location: UG40, School of Computer Science Title: TBA Speaker: Hongseok Yang Institution: Queen Mary University of London Host: Uday -------------------------------- Date and time: Friday 12th October 2007 at 14:00 Location: UG40, School of Computer Science Title: On Metric Temporal Logic and Faulty Turing Machines Speaker: Joel Ouaknine Institution: Oxford University Host: Achim Abstract: I will present some recent results about Metric Temporal Logic (MTL), a prominent real-time extension of the temporal logic LTL. In doing so I will discuss surprisingly strong connections between MTL and certain kinds of faulty Turing machines, which are themselves of independent interest. This is joint work with James Worrell. -------------------------------- Date and time: Friday 19th October 2007 at 14:00 Location: UG40, School of Computer Science Title: Algebraic Semantics for Typed Effects Speaker: Bob Atkey Institution: University of Edinburgh Abstract: We consider the problem of giving a useful denotational semantics to type and effect systems. We extend Plotkin and Power's interpretation of effectful programs as elements of a free universal algebra to incorporate type information that restricts the effects that are allowed at any point in the program. By relating our typed semantics to the usual untyped semantics we can derive useful program equivalences permitted by the type system. These equivalences have previously been proved using an extensional relational semantics by Benton, Kennedy, Hofmann and Beringer. We provide an intensional method of proving such equivalences that extends easily to other kinds of effects. -------------------------------- Date and time: Friday 26th October 2007 at 14:00 Location: UG40, School of Computer Science Title: Linearity and Optimality Speaker: Ian Mackie Institution: King's College Host: Dan Ghica Abstract: In this talk I will present some new ideas and partial solutions on implementing the lambda calculus. We first re-examine notions of optimality for the linear case, and then show a variety of methods that can be used to extend these results to the general case. This work is leading towards a new theory of optimal reduction for the lambda calculus based on geometry of interaction style implementations. -------------------------------- Date and time: Friday 2nd November 2007 at 14:00 Location: UG40, School of Computer Science Title: Formal verification of ARM software and hardware Speaker: Mike Gordon Institution: University of Cambridge Host: Dan Ghica Abstract: A microarchitecture can be shown to implement an instruction set architecture (ISA) by proving formally that for all possible inputs and initial memory states the microarchitecture and ISA have corresponding executions. Such proofs amount to verifying compliance for all possible test suites and are used for high assurance certification (e.g. Common Criteria Evaluation Assurance Level 7). Some years ago, as part of a project involving Graham Birtwistle, Dominic Pajak and Daniel Schostak, Anthony Fox verified that the ARMv3 ISA was correctly implemented by the ARM6 microarchitecture. The ISA specification has subsequently been updated to ARMv4 (ARMv5 planned). I will explain how such processor correctness proofs are formulated and discuss the kind of software tools needed to carry them out. I'll mainly talk about work done at Cambridge, but will mention related work at Intel, AMD and Rockwell Collins. Recently we have been doing work to develop methods for formally verifying assembly code implementations of the core operations of elliptic curve cryptography. We are using our ARM ISA model as the semantics for assembly code, and are building verified higher levels models on top of it. My talk will be based on one given at ARM and is a high-level overview of past and current work. -------------------------------- Date and time: Friday 9th November 2007 at 14:00 Location: UG40, School of Computer Science Title: Local Reasoning for Storable Locks and Threads Speaker: Josh Berdine Institution: Microsoft Research, Cambridge Host: Hayo Thielecke Abstract: This talk will present a resource-oriented program logic that is able to reason about concurrent heap-manipulating programs with unbounded numbers of dynamically-allocated locks, and note an extension to storable threads. The logic is inspired by concurrent separation logic, but handles these more realistic concurrency primitives. We demonstrate that the proposed logic allows for local reasoning about programs that exhibit a high degree of information hiding in their locking mechanisms. Soundness is proved using a novel thread-local fixed-point semantics. -------------------------------- Date and time: Friday 16th November 2007 at 14:00 Location: UG40, School of Computer Science Title: Categorical Aspects of Locale Theory Speaker: Christopher Townsend Host: Steve Vickers Abstract: The purpose of the talk is to try and describe aspects of locale theory that are available using only categorical reasoning. Some basic 'facts about locales' will be recalled and then we will cover various results from locale theory using only these 'facts about locales' as categorical assumptions. The plan is to cover the results: pullback stability of (maps with) weak triquotient assignments, the Hofmann-Mislove theorem, the closed subgroup theorem, the patch construction, Hyland's result and a representation theorem for geometric morphisms. Only outlines will be given. It will be assumed that the audience is familiar with what the category of locales is; for example knowing what the upper and lower power locale monads are. It will also be assumed that the audience has some knowledge of Compact/Open duality in locale theory; i.e., broadly, that the theory of proper maps is the same thing as the theory of open maps but with preframe homomorphisms in the place of suplattice homomorphisms and with the order enrichment reversed. So, open subobject is dual to closed subobject and, further, the notion of 'compact object' is dual to the notion of 'open object' under Compact/Open duality. -------------------------------- Date and time: Friday 23rd November 2007 at 14:00 Location: UG40, School of Computer Science Title: Adaptive shape analysis Speaker: Dino Distefano Institution: Queen Mary University of London Host: Dan Ghica Abstract: I will introduce a new program analysis technique that supports complex heap-allocated data-structures found in industrial programs. Examples of such data-structures include ``singly-linked lists of cyclic doubly-linked lists'', ``singly-linked lists with back-pointers to head nodes'', etc. The analysis uses higher-order inductive predicates to describe heap-allocated data structures and a method of synthesizing new predicates on-the-fly. The result is an adaptive shape analysis which can describe data-structures unique to the program being analyzed. I will also discuss our experience when applying the proposed approach to examples drawn from Windows device drivers. -------------------------------- Date and time: Friday 30th November 2007 at 14:00 Location: UG40, School of Computer Science Title: Verification of Infinite Structures: A Semantic Approach Speaker: Luke Ong Institution: Oxford University Abstract: Starting from the 80's, the computer-aided verification of finite-state systems (e.g. digital hardware and communication protocols) is a great success story in computer science. A focus of the past decade has been the transfer of these techniques to finitely-generated infinite structures that are useful for program verification. We consider two families of generators: higher-order (collapsible) pushdown automata on the one hand, and higher-order recursion schemes on the other. Each family can serve as a definitional device for the respective hierarchies of word languages, infinite trees, and infinite graphs. These infinite structures give rise to accurate models of computation for higher-order procedural programs. We survey recent advances in the algorithmic (especially model checking) properties of these hierarchies, and consider the close relationship between the two families of generators, as mediated by game semantics. A theme of the talk is the fruitful interplay of ideas and methods between the neighbouring fields of semantics and verification. -------------------------------- Date and time: Friday 7th December 2007 at 14:00 Location: UG40, School of Computer Science Title: Topos theory in the foundations of physics Speaker: Andreas Doering Institution: Imperial College, London Host: Steve Vickers Abstract: It is known from the Kochen-Specker theorem that there is no naive realist picture of quantum theory. In this talk, I will show how the use of topos theory can lead to a `neo-realist' formulation in which all propositions about the values of physical quantities have truth-values. In this approach, a certain presheaf takes the rôle of a generalised state space. Spitters and Heunen recently observed that this basically is the internal Gel'fand spectrum (of the algebra of physical quantities) as defined by Mulvey and Banaschewski. -------------------------------- Date and time: Friday 14th December 2007 at 14:00 Location: UG40, School of Computer Science Title: Coq: A survey on the history, achievements and features. Speaker: Theo Tsokos Institution: University of Birmingham Abstract: Initially started as an implementation of the Calculus of Constructions 25 years ago, the Coq System is - something more than - a proof assistant and indisputably a widely evolved powerful tool. Coq, can be used to model specifications and to develop software that can be verified under these specifications. It can also be used as a proof developer, with its higher order logic and extensive libraries. Furthermore, in the last few years, formalizations of Java in Coq, program certification using Coq and large programming projects in Coq, along side with the constant evolution of its libraries and optimizations of the system, show its capabilities and its wide potential. In this presentation, a brief history of Coq and an introduction to its background calculus will be shown. Thereafter, a demonstration of the system and a short survey on the achievements of Coq in academia and industry will take place. This seminar is accessible to a non-specialist audience. -------------------------------- Date and time: Tuesday 18th December 2007 at 14:00 Location: UG40, School of Computer Science Title: MGS Christmas seminar Speaker: S Peyton-Jones, D Ghica, H Nilsson Institution: MGS Abstract: 14:00h-15:00h Static contract checking for Haskell Simon Peyton Jones, Microsoft Research (joint with Dana Xu, Cambridge Computer Lab) Modern type systems (eg in Haskell and ML) exclude many bugs by construction. But not all! We would like to go beyond these type systems, and write down the pre and post-conditions of our functions. More generally, in a higher-order language like Haskell, we extend traditional pre/post conditions to so-called "contracts. Then we are faced with questions like * What does it mean, precisely, for a function to 'satisfy a contract'? * How can we statically verify that it satisfies the contract? * What if the contract itself violates the contracts of the functions it calls? In my talk I'll describe work in progress that makes some progress on these questions, in the context of Haskell. Our goal is to extend the "reach" of static verification, beyond traditional type systems, and to do so in a way that ordinary programmers (without PhDs) can make sense of. 15:00h-15:30h Coffee 15:30h-16:30h Geometry of Synthesis: A structured approach to VLSI design Dan Ghica, University of Birmingham I propose a new technique for hardware synthesis from higher-order functional languages with imperative features based on Reynolds's Syntactic Control of Interference. The affine type system is useful for managing the thorny issue of sharing in physical circuits. We use a semantic model inspired by game semantics and the geometry of interaction, and express it directly as a certain class of digital circuits that form a cartesian, monoidal-closed category. Based on this theoretical foundation we introduce a new ANSI C to hardware compiler and we discuss some methodological issues regarding the role of higher order programming languages in hardware design. 16:30h-17:30h Switched-on Yampa: Programming Modular Synthesizers in Haskell Henrik Nilsson, University of Nottingham In this talk and demonstration, we present an implementation of a modular synthesizer in Haskell using Yampa. A synthesizer, be it a hardware instrument or a pure software implementation, as here, is said to be modular if it provides sound-generating and sound-shaping components that can be interconnected in arbitrary ways. Yampa, a Haskell-embedded implementation of Functional Reactive Programming, supports flexible construction of hybrid systems. Since music is a hybrid continuous-time and discrete-time phenomenon, Yampa and is a good fit for such applications, offering some unique possibilities compared to most languages targeting music or audio applications. The demonstration illustrates this point by showing how simple audio blocks can be described and then interconnected in a network with dynamically changing structure, reflecting the changing demands of a musical performance. -------------------------------- Date and time: Friday 11th January 2008 at 14:00 Location: UG40, School of Computer Science Title: Towards automatic verification of fine-grained concurrency Speaker: Viktor Vafeiadis Institution: Cambridge University Host: Uday Abstract: In this talk, I will introduce RGSep, a program logic that combines rely/guarantee and separation logic. In RGSep, we can describe interference naturally (using a relation as in rely/guarantee), and where there is no interference, we can reason locally (as in separation logic). As a result, we can construct relatively simple proofs of quite complex concurrent algorithms. Time permitting, I will conclude with a demonstration of SmallfootRG, an automatic verification tool based on RGSep. -------------------------------- Date and time: Friday 18th January 2008 at 16:00 Location: UG40, School of Computer Science Title: A games model of bunched implications Speaker: Guy McCusker Institution: University of Bath Abstract: A game semantics of the (--*, -->) fragment of O'Hearn and Pym's Logic of Bunched Implications (BI) is presented. The model is based on Hyland-Ong-style innocent strategies, augmented with new conditions to capture the resource control aspects of the logic. It is shown that the model has the property of full completeness; that is, every finite element of the model is the denotation of a proof of BI. This is joint work with David Pym (HP Labs, Bristol). -------------------------------- Date and time: Friday 1st February 2008 at 14:00 Location: UG40, School of Computer Science Title: Logics for Coalgebras Speaker: Alexander Kurz Institution: University of Leicester Abstract: Coalgebras for a functor F generalize transition systems. Coalgebraic logic aims at extending this uniform approach to logics of transition systems. In this talk, I will address the question of how to associate to any set-functor F a corresponding logic, together with a complete calculus. This can be achieved by associating to each F a `dual' functor L on Boolean algebras, which encodes a modal logic for F-coalgebras. This functorial view of a modal logic leads to an elegant abstract account of modal logics. On the one hand, the syntax and proof calculus of the logic are given by a presentation of the functor L. On the other hand, theorems about the logic can be proved independently of any particular presentation. As examples, the classic theorems of Jonsson-Tarski and Goldblatt-Thomason will be discussed. [From joint work with M. Bonsangue and with J. Rosicky] -------------------------------- Date and time: Friday 8th February 2008 at 14:00 Location: UG40, School of Computer Science Title: The three Platonic models of CSP Speaker: Bill Roscoe Institution: Oxford University Host: Paul Levy Abstract: Traces and failures are best known types of finitary observation that go to make up CSP's behavioural models, but there are a number of others known. In particular the idea of revivals -- (s,X,a) where the process performs the traces, stably refuses X and then performs a (not in X) -- has recently been developepd into a family of models by the author. In this talk I will show how, both in the class of models where only finite behaviours are observed and in the class with strict divergence, are an inevitable initial sequence: every model that is not one of these three refines revivals. -------------------------------- Date and time: Friday 15th February 2008 at 14:00 Location: UG40, School of Computer Science Title: The Finite Model Theory of Tame Classes of Structures Speaker: Anuj Dawar Institution: University of Cambridge Host: Achim Jung Abstract: The early days of finite model theory saw a variety of results establishing that the model theory of the class of finite structures is not well-behaved. Recent work has shown that considering subclasses of the class of finite structures allows us to recover some good model-theoretic behaviour. This appears to be especially true of some classes that are known to be algorithmically well-behaved. I will review some results in this area and explore the connection between logic and algorithms. -------------------------------- Date and time: Friday 22nd February 2008 at 14:00 Location: UG40, School of Computer Science Title: Deriving structural labelled transitions for mobile ambients Speaker: Pawel Sobocinski Institution: University of Southampton Host: Paul Levy Abstract: We will present a new LTS for the ambient calculus on which ordinary bisimilarity coincides with contextual equivalence. Its key feature is that it is the fruit of ongoing work on developing a systematic procedure for deriving LTSs in the structural style from the underlying reduction semantics and observability. Soundness of the bisimilarity for contextual equivalence follows from the construction and there is an easy way of obtaining completeness. -------------------------------- Date and time: Friday 29th February 2008 at 14:00 Location: UG40, School of Computer Science Title: Slicing Object Code Speaker: Jan Muehlber Institution: York University Host: Dan Ghica Abstract: Slicing is a widely deployed technique for abstracting over program details that are irrelevant when automatically validating some desired property of the program. Unfortunately, most published slicing algorithms work on source code and are thus not applicable to software that is only available in object code form. This talk presents a novel technique for slicing object code that retains the executability of the resulting slice. The underlying approach is based on an intermediate representation that is borrowed from the binary instrumentation framework Valgrind. Our slicing technique lends itself to synthesising models from compiled programs, in order to reduce execution times for subsequent simulation, verification and testing. We have implemented a prototype object-code slicer as a front-end of a bounded model-checking tool that checks operating systems software for memory safety. Our results show that object-code slicing drastically reduces verification time and speeds-up code execution when using real Linux device drivers as benchmark. -------------------------------- Date and time: Friday 7th March 2008 at 14:00 Location: UG40, School of Computer Science Title: Local Hoare reasoning about DOM Speaker: Philippa Gardner Institution: Imperial College Abstract: The W3C Document Object Model (DOM) specifies an XML update library. DOM is written in English, and is therefore not compositional and not complete. We provide a first step towards a compositional specification of DOM. Unlike DOM, we are able to work with a minimal set of commands and obtain a complete reasoning for straight-line code. Our work transfers O’Hearn, Reynolds and Yang’s local Hoare reasoning for analysing heaps to XML, viewing XML as an in-place memory store as does DOM. In particular, we ap- ply recent work by Calcagno, Gardner and Zarfaty on lo- cal Hoare reasoning about a simple tree-update language to DOM, showing that our reasoning scales to DOM. Our reasoning not only formally specifies a significant subset of DOM Core Level 1, but can also be used to verify e.g. in- variant properties of simple Javascript programs. -------------------------------- Date and time: Friday 4th April 2008 at 14:00 Location: UG40, School of Computer Science Title: TBA Speaker: Michael Mendler Institution: Bamberg Host: Eike Ritter -------------------------------- Date and time: Friday 30th May 2008 at 16:00 Location: UG40, School of Computer Science Title: Better Model Driven Architecture through Constructive Type Theory Speaker: Iman Poernomo Institution: King's College London Abstract: Model Driven Architecture (MDA) is a methodology based on the Meta Object Framework (MOF) to develop software by means of successive refinements from abstract platform-independent models to concrete platform-specific models. The purpose is to promote a clear demarcation of abstract architecture and implementation-specific issues. Central to MDA is the ability to define transformations as mappings between metamodels. Such transformations are powerful, providing a systematic means of model refinement. They are also dangerous: a single error in a transformation mapping can result in the systematic introduction of a range of errors in a resulting model. This talk explores a way of solving this problem through a formalisation of metamodel transformations within constructive type theory. -------------------------------- Date and time: Tuesday 8th July 2008 at 16:00 Location: UG40, School of Computer Science Title: Graph Calculi for Algebras of Relations Speaker: Jorge Petrucio Viana Institution: Universidade Federal Fluminense Abstract: We present a sound and complete logical system for decide the valid inclusions between graphs and extend it to deriving inclusions between graphs from inclusions between graphs, taken as hypotheses. This leads to a system dealing with complementation. Graphs provide a natural tool for expressing relations and reasoning about them. We apply our system to standard relational formalisms considering some examples took from the theory of relation algebras. -------------------------------- Date and time: Friday 11th July 2008 at 15:00 Location: UG40, School of Computer Science Title: Coalgebra and Recursion Speaker: Larry Moss Institution: University of Indiana Host: Achim Abstract: The main objects of study in coalgebra are generalizations of transition systems and related models; the intuitions with coalgebra are related to 'observation' while those in algebra are closer to 'transformation', 'operation', and the like. Computation, of course, has both aspects. In a sense, this talk is about the project of bringing the two together. On a technical level, I'll present recent results on recursive program schemes obtained together with Stefan Milius. Our work gives a very general approach to recursive definitions based on coalgebra and Elgot algebra. (I'll go over these in detail of course.) It also is connected to fixed point definitions of sets and functions in continuous mathematics, and to logics for reasoning about recursive program schemes. -------------------------------- Date and time: Friday 19th September 2008 at 16:00 Location: UG40, School of Computer Science Title: an unambiguous temporal logic Speaker: Kamal Lodaya Institution: The Institute of Mathematical Sciences, Chennai Abstract: interval temporal logic is a highly expressive and succinct logic whose satisfiability over words is non-elementary. we define a sublogic of interval logic by replacing the chop operator with marked, deterministic chop operators. the resulting logic admits unique parsing of a word matching a formula, with the consequence that membership is in polynomial time (in fact, in the complexity class logdcfl) and satisfiability is in polynomial space (and np-complete over a fixed alphabet). we show model-preserving reductions between the logic and the partially ordered two-way automata introduced by schwentick, therien and vollmer. it follows from the work of schutzenberger, therien and wilke that our logic has the same expressive power over words as first-order logic with two variables. the talk is joint work with paritosh pandya and simoni shah at tifr, mumbai, and was presented at the ifip tcs conference in milano earleir this month. -------------------------------- Date and time: Friday 26th September 2008 at 14:00 Location: UG40, School of Computer Science Title: Focusing on Pattern Matching Speaker: Neel Krishnaswami Institution: Carnegie Mellon Host: Paul Levy Abstract: From the point of view of the semanticist, one of the chief attractions of functional programming is the close connection of the typed lambda calculus to proof theory and logic via the Curry-Howard correspondence. The point of view of the workaday programmer seems, at first glance, less exalted -– one of the most compelling features in actual programming languages like ML and Haskell is the ability to analyze structured data with pattern matching. But pattern matching, though enormously useful, has historically lacked the close tie to logic that the other core features of functional languages possess. The Definition of Standard ML, for example, contains a suggestion in English that it would be desirable to check coverage, with no clear account of what this means or how to accomplish it. In this talk we will argue the semanticist ought to be just as interested in pattern matching as the programmer. We show that pattern matching has a strong logical interpretation via the proof-theoretic notion of focusing, and that filling in this part of the Curry-Howard correspondence enables simple correctness proofs of parts of the compiler (such as the coverage checker and the pattern compiler) that required considerable insight and creativity before. -------------------------------- Date and time: Friday 3rd October 2008 at 14:00 Location: UG40, School of Computer Science Title: Thread-modular heap analysis Speaker: Alexey Gotsman Institution: University of Cambridge Host: Hayo Abstract: We present a static analysis for verifying memory-safety and data race freedom properties of multithreaded programs that avoids the explicit enumeration of execution-interleavings. Our analysis is inspired by concurrent separation logic and is based on automatic inference of a resource invariant associated with each lock that describes the part of the heap protected by the lock. This allows us to use a sequential static analysis on each thread. Experiments with applying our prototype implementation to concurrent heap-manipulating code from Windows device drivers show that the analysis is precise and scalable. This is joint work with Josh Berdine, Byron Cook and Mooly Sagiv. -------------------------------- Date and time: Friday 24th October 2008 at 14:00 Location: UG40, School of Computer Science Title: Cryptographic Protocol Composition via the Authentication Tests Speaker: Joshua Guttman Institution: The MITRE Corporation Host: Ben Abstract: Although cryptographic protocols are typically analyzed in isolation, they are used in combinations. If a protocol was analyzed alone and shown to meet some security goals, will it still meet those goals when executed together with a second protocol? While not every choice of a second protocol can preserve the goals, there are syntactic criteria for the second protocol that ensure they will be preserved. Our main result strengthens previously known criteria. Our method has three main elements. First, a language L(Pi) in classical logic describes executions of each protocol Pi, and expresses its security goals. Strand spaces provide the models for L(Pi). Second, the strand space ``authentication test'' principles suggest our syntactic criterion for security goals to be preserved. Third, certain homomorphisms among models for L(Pi) preserve the truth of formulas of the syntactic form that security goals take. This provides a way to extract -- from a counterexample to a goal that uses both protocols -- a counterexample using only the first protocol. Our essentially model-theoretic technique studies a syntactically defined set of formulas using the homomorphisms among their models. It appears to be novel for protocol analysis. -------------------------------- Date and time: Friday 7th November 2008 at 14:00 Location: UG40, School of Computer Science Title: Interacting quantum observables Speaker: bob coecke Institution: Oxford University Computing Laboratory Abstract: Joint work with Ross Duncan, ICALP'08. Within a high-level category-theoretic framework, as well as in terms of an intuitive purely diagrammatic calculus, we axiomatise an essential feature of quantum mechanics. This feature is the interaction of incompatible of quantum observables. A typical example is the interaction of position and momentum. Axiomatic approaches to quantum mechanics have historically focussed on the failure of various properties: non-commutative algebras, non-distributive lattices, non-Kolmogorovian probabilities, etc. More recent attempts, originating in quantum computer science, concentrate mainly on accommodating no-cloning and no-deleting. Here we take a positive attitude: we identify the flows of information between incompatible observables. We show that a pair mutually unbiassed quantum observables forms a bialgebra-like structure. Additional structure enables us to derive all observables and define a computationally universal system. The resulting equations suffice to perform intuitive computations with elementary quantum gates, translate between distinct quantum computational models, establish the equivalence of entangled quantum states, and simulate quantum algorithms such as the quantum Fourier transform. -------------------------------- Date and time: Friday 21st November 2008 at 14:00 Location: UG40, School of Computer Science Title: Streaming semantics for the Gannet heterogeneous multicore processor Speaker: Wim Vanderbauwhede Institution: University of Glasgow Host: Dan Abstract: Gannet is a framework for high-level design of heterogeneous multicore Systems-on-Chip (SoC). From a theoretical perspective, the Gannet SoC is a demand-driven coarse-grained distributed dataflow machine. Gannet uses a functional language paradigm to program the machine at high level. A particular problem with multicore machines is efficient streaming data processing: to use the full potential of a multicore machine, the cores should operate in parallel on different portions of the data stream. This concept (pipelining) is well-know in hardware design but much less common in software design as the von Neumann model is essentially sequential. In this talk I will present a small-step operational semantics for the Gannet machine and use this semantics to explain streaming data processing and relate it to the Gannet language. -------------------------------- Date and time: Friday 12th December 2008 at 14:00 Location: UG40, School of Computer Science Title: Permission-based separation logic for message passing concurrency Speaker: Julian Rathke Institution: University of Southampton Host: Paul Levy Abstract: We develop local reasoning techniques for message passing concurrent programs based upon ideas from separation logics and resource usage analyses. We proposed a two-step analysis in which concurrent processes are first analysed for confluent behaviour using a type and effect system. This analysis provides a foundation for establishing correctness through logical, separation-based reasoning. -------------------------------- Date and time: Friday 16th January 2009 at 14:00 Location: UG40, School of Computer Science Title: Synthesis of Second-Order Equational Logic Speaker: Marcelo Fiore Institution: University of Cambridge Abstract: I will present a mathematical methodology for the synthesis of equational deduction systems that are sound and internally complete for a canonical algebraic model theory; see [1]. As a running example, I will indicate how the methodology applies to rationally reconstruct the traditional equational logic of universal algebra from general principles; see [3 (Part I)]. As for a modern application, I will use the methodology to synthesise a second-order equational logic for specifying simple type theories; see [2 (Part I)] and [3 (Part II)]. This is joint work with my student Chung-Kil Hur. References [1] Marcelo Fiore and Chung-Kil Hur. Term equational systems and logics. In 24th Mathematical Foundations of Programming Semantics Conf. (MFPS XXIV), 2008. Paper: [2] Marcelo Fiore. Second-order and dependently-sorted abstract syntax. In Logic in Computer Science Conf. (LICS'08), pages 57-68. IEEE, Computer Society Press, 2008. Paper: Slides: [3] Marcelo Fiore. Algebraic theories and equational logics. Invited tutorial at the 24th Mathematical Foundations of Programming Semantics Conf. (MFPS XXIV), 2008. Notes: -------------------------------- Date and time: Friday 23rd January 2009 at 14:00 Location: UG40, School of Computer Science Title: Logics for Unranked Trees: An Overview Speaker: Leonid Libkin Institution: University of Edinburgh Abstract: Labeled unranked trees are used as a model of XML documents, and logical languages for them have been studied actively over the past several years. Such logics have different purposes: some are better suited for extracting data, some for expressing navigational properties, and some make it easy to relate complex properties of trees to the existence of tree automata for those properties. Furthermore, logics differ significantly in their model-checking properties, their automata models, and their behavior on ordered and unordered trees. In this talk I present a survey of logics for unranked trees. -------------------------------- Date and time: Friday 6th February 2009 at 14:00 Location: UG40, School of Computer Science Title: Identity types and weak factorisation systems Speaker: Nicola Gambino Institution: University of Leicester Abstract: Since the work of Robert Seely in the '80s, it is well-known that extensional dependent type theories have a sound and complete semantics in locally cartesian closed categories. For intensional dependent type theories, instead, the definition of a satisfactory semantics is still an open problem. A key issue is the interpretation of Martin-Lof's rules for identity types. I will describe a new approach to the problem, originating in work of Awodey and Warren, which is based on surprising connections with abstract homotopy theory. In particular, I will describe joint work with Richard Garner, showing how the rules for identity types give rise to a a weak factorisation system on the syntactic category arising from Martin-Lof type theory. I will not assume any background of homotopy theory. -------------------------------- Date and time: Friday 13th March 2009 at 14:00 Location: UG40, School of Computer Science Title: Towards Parametric Direcursion Speaker: Johan Glimming Institution: University of Cambridge Host: Achim Abstract: I will speak about Freyd's universal property generalising that of initial algebras and final coalgebras. This property, termed direcursion, appears to be useful in programming language semantics. For example, typical models of untyped lambda calculus and of object-based programming languages come equipped with this property. Recent work on higher-order store have used recursive domain equations giving rise to the same property. We here begin to develop a new reasoning principle with an aim to allow both constant and modifiable (accumulating) parameters. In the case of initial algebras, it is known since work by Spencer that strong functors, i.e. functors equipped with a natural transformation distributing a product over the endofunctor, gives rise to a parametric version of iteration in a cartesian closed category. We therefore ask how the situation generalises to mixed-variant bifunctors and direcursion, and what universal property arises in this more general circumstance. It turns out that we require a generalisation of strength, called distrength, in addition to monoidal closed structure. Existence and uniqueness of solutions are demonstrated -------------------------------- Date and time: Thursday 16th April 2009 at 14:00 Location: UG40, School of Computer Science Title: Remarkable properties of monads related to the semantics of non-determinism Speaker: Matias Menni Institution: Universidad Nacional de La Plata Host: Martin Escardo Abstract: Let M = (M, m, u) be a monad and let (M A, m) be the free M-algebra on the object A. Assume that the canonical presentation a : (M A, m) -> (A, a) of the algebra (A, a) has a section s : (A, a) -> (M A, m). The retract (A, a) is not free in general. We observe that for many monads with a `combinatorial flavor' such a retract is not only a free algebra (M A0 , m) but it is also the case that the object A0 of generators is determined in a canonical way by the section s. We give a precise form of this property and explain its combinatorial motivation by discussing several examples, among these, compact convex spaces. -------------------------------- Date and time: Friday 24th April 2009 at 14:00 Location: UG40, School of Computer Science Title: The Reduceron Speaker: Matthew Naylor Institution: University of York Host: Dan Abstract: Efficient evaluation of high-level functional programs on conventional computers is a big challenge. Sophisticated implementation techniques are needed to exploit architectural features designed for low-level imperative execution. What's more, conventional computers have inherent limitations when it comes to running functional programs. In this talk, I will explore what is possible when some of these constraints and limitations are lifted. I will do so with reference to the Reduceron, a special-purpose reduction machine for lazy functional languages, prototyped on an FPGA. I will focus on some architectural features that allow for an efficient yet simple implementation. -------------------------------- Date and time: Tuesday 5th May 2009 at 14:00 Location: LG33, Learning Centre Title: Finite Sequential Procedures with observational ordering Speaker: Dag Normann (http://www.math.uio.no/~dnormann/) Institution: Department of Mathematics, The University of Oslo, Blindern, N-0316 Oslo, Norway (http://www.math.uio.no/) Host: Martin Escardo Abstract: The sequential functionals of finite types with the observational ordering serve as a fully abstract model for PCF. They can be viewed as objects in Milner's fully abstract model based on Domain Theory, but have over the last 10-15 years been characterized in other ways as well. For many years it was an open problem if the sequential functionals forms directed complete partial orderings, which would mean that all objects in Milner's model are sequential, but in 2004 Normann showed that this is not the case. This result led Sazonov to conjecture that there are sequential functionals that are compact in Milner's model, but not if we restrict the attention to the sequential objects, and that not all sequential functionals commute with least upper bounds within the sequential functionals. In this lecture, I will introduce the Finite Sequential Procedures and construct the sequential functionals as standard parts of Hyperfinite Sequential Procedures. I will show that Sazonov's conjectures hold and discuss the frequency of the phenomena suggested by the conjectures. We will, for instance, see that even for non-pure types at level 2 the sequential functionals do not form dcpo's. The technical results are joint with Vladimir Sazonov at the University of Liverpool. -------------------------------- Date and time: Friday 29th May 2009 at 14:00 Location: UG40, School of Computer Science Title: An analysis of innocent interaction Speaker: Russ Harmer Institution: Universite de Paris 7 Host: Dan Abstract: We will present an analysis of the process of interaction between innocent strategies, leading to a new class of cellular strategies with an associated abstract machine, the CPAM, which radically simplifies the usual machines for innocent interaction (PAM, VAM, GAM, etc). We will then describe a cellularization process, mapping an innocent strategy to a cellular strategy, that allows us to simulate the usual machines by first cellularizing and then using the CPAM. If time permits, we will also explain the connection of this work with the use of a distributive law (!?A -o ?!A) to construct the category of innocent strategies. -------------------------------- Date and time: Friday 12th June 2009 at 14:00 Location: UG40, School of Computer Science Title: Events, Causality and Symmetry Speaker: Glynn Winskel Institution: University of Cambridge Host: Dan Abstract: This talk will try to motivate, explain and delineate a research programme in causal models, such as event structures and Petri nets, and how through the introduction of a formal treatment of symmetry such models connect with the broader mathematical world of (higher-dimensional) algebra. The work on which the programme is based began through attempts to provide an operational reading to presheaf models for concurrent processes.