I'm no longer employed at Middlesex. But I'm going to become a Visiting Prof, so I've kept my email address. I expect in the future to continue my research on why so many people can't learn to program (see below) with Ray Adams.
I've been working, with Hasan Amjad, on trying to produce an understandable/believable proof of Simpson's and Harris's multi-slot single-place non-blocking buffer algorithms. In particular we have a nice refinement development. See separation logic for the latest version.
In separation logic, a proof of the frying pan list reversal. Elsewhere, a free copy of my old book on compiling.
Saeed Dehnadi's work on predicting programming aptitude (see his web site) continues to progress. He passed his PhD exam with minor corrections, which are now underway.
Jape continues to exist and to be maintained.
Hasan and I spent a solid year crawling over Simpson's algorithm, the famous four-slot non-blocking buffer, and Harris's algorithm, a less famous three-slot version. By coincidence so have Cliff Jones and Jean-Raymond Abrial. I think I now understand the algorithm and can say why it works. Our latest explanation is by refinement and linearisability (we are considering submitting it to FACJ, and for the moment have typeset it in their style). There is also an earlier paper, which is forthcoming in FACJ, and may be interesting as a practical introduction to reasoning in Vafeiadis and Parkinson's RGSep logic (rely-guarantee meets separation logic and gets married).
Cyclic Proofs of Termination in Separation Logic (lead author James Brotherston, with me and Cristiano Calcagno), published in POPL 2008. Includes a termination proof (hurrah!) of the frying-pan-list reversal problem.
Modular verification of a non-blocking stack (lead author Matthew Parkinson, with me and Peter O'Hearn) presented at POPL 2007. Really it's Matthew's proof.
Variables as resource in Separation Logic (with Cristiano Calcagno and Hongseok Yang), presented at MFPS XXI 2005, proposed a treatment of variables as resource in separation logic. It was more or less ok, but Variables as resource in Hoare Logic (lead authors Matthew Parkinson and Cristiano Calcagno, with me too), presented at LICS 2006, tidied it up and gives a soundness proof.
A survey paper written for an LNCS volume to be produced by the BCS FACS interest group, covering concurrent separation logic up to about January 2006, and including a sketched proof of Simpson's 4-slot algorithm (joint work with Matthew Parkinson).
Paper on permission accounting: delivered at POPL 2005.
Slides on resourcing: includes permission accounting, a mention of variables as resource, and a grand challenge (resourcing is the wave beyond typing!).
Here are the slides for a lecture which I gave to MSc students at Mdx in Feb 2004, in an attempt to attract research interest. The illustrations of the Unix v5 block cache are very sketchy, and don't represent the beauty and horror of the original. (The original source code is available at the Unix Archive, and the bug is there all right, but it doesn't look like what I remembered. My memory must have simplified things.)
Local reasoning, separation and aliasing (delivered at SPACE 04, Venice) contains proofs of fringe linking, copyDAG, copygraph and disposegraph -- small recursive algorithms that deal with internally aliased graph structures.
Reasoning about pointer programs in Hoare logic -- not separation logic really, but it's about separation. My contribution to kickstarting the whole business was to talk loudly about separation, to make some proofs, and to coin some slogans. (I still have the Japeish proofs that back up this paper, but I've temporarily mislaid them. Contact me if you want a look.)
Jape, despite my best efforts, won't die. I've written a book (Formal Proof and Disproof, OUP, 2005) and produced new version after new version, but it keeps rolling on regardless.
Bernard Sufrin left the project years ago, but we remain best friends and he is the only person who is prepared to discuss the design of Jape with me (I do have an email address, you know: see the top of the page). By accident, he ran the Jape website at Oxford, and by laziness, it's still there (but not always up, because Oxford are a bit afflicted with security-itis). I mean to move it to Middlesex (the machine I shall use is out of the reach of CCSS), and that will probably happen early 2006.
A paper summarising the developments in Jape over the last few years. A conflation of two papers which I gave at the Rome UITP workshop in 2001, but didn't put in the proceedings (for reasons too stupid to reveal).
I've done a new Roll Your Own (which is on the website in DOCUMENTS but not yet in the distributions), a new Natural Deduction manual (which is in the distribs, I think), there's a new Hoare logic for the book, and of course it works under MacOS X, Windoze and Linux and Solaris. (Actually on MacOS X you have to use a Micros**t font, because the STIX fonts people keep pushing their deadline back -- they are only a couple of years late -- but Real Soon Now you will be able to see Jape multi-platform with all the symbols, even the BAN logic ones, for the first time, and it will all be open source.)
Jape's gone GPL at last and the entire source is at sourceforge.
Feedback and bug reports (there might be bugs, you never know!) to me, please, at the address at the top of this page. (Bernard currently owns bugs@jape.org.uk and I think he forwards everything to me, but it isn't automatic.)
A video of a rather overweight me dancing the proof of circular list reversal on Aldeburgh beach. Cameraman and knee: Cristiano Calcagno. Directors: Peter O'Hearn and Josh Berdine.
My inaugural lecture "The littlest birds sing the prettiest songs" (acknowledgements to the Be Good Tanyas for the title) is sometimes asked for. It fell off the Mdx website a while ago: here it is.
I get requests, every now and then, for lecture notes and the like. Notes on logic were turned into a book; notes on compiling into an earlier book; notes on algorithms are here.
In the late 1970s I wrote a book on compiling which was a success. People still ask me for copies. Now that even Abebooks has run out, and since I recovered the copyright, I've converted it as lightly as I can to Latex and put a pdf online. Here it is -- with hyperlinks so it's easy to read online (but beware! 2.55 MB).
I also have a private home page. With a nicer picture.