Contents of this page: Photos | Local information | Proposed topics for discussion | Proposed talksMinutes of the meeting are now available (last updated 3rd May 2006).
Interrupts are important for writing robust, modular programs, but are traditionally viewed as being difficult from a semantic perspective. In this talk we present a simple, formally justified, semantics for interrupts. Our approach is to consider a minimal high-level language and a minimal low-level machine with support for interrupts, give each a semantics, and then relate these semantics via a compiler. In this manner we obtain two different perspectives on the problem, formally shown to be equivalent, which gives greater confidence in the correctness of our semantics.Slides are also available. (Joint work with Joel Wright.)
This is a sort of a continuation of my last talk at Nottingham. During that talk, Neil Jones asked me if I could write a fifol program which simulates a fifol machine. I began to hack programming realize it and I found my solution interesting.
A (partial) function f has a left inverse f^{-1} if f^{-1} . f = dom f. Consider simply typed lambda calculus where lambda expressions define partial functions from terms to terms. In this talk, we will propose a calculus which allows one to derive answers to the following questions: what is the left inverse of the K combinator, the B combinator, or C I (= \x y . y x)? In the future we hope to be able to deal with recursion and talk about, for example, the inverse of the function "map".The research is currently in a very preliminary stage. On the other hand, the good news is that it does not seem to rely on any particular theory, which means that everyone can get involved!