Richard Bornat (Middlesex page)

email: R DOT Bornat AT mdx DOT ac DOT uk (come, friendly AI bots and spam me).

After some considerable time I've updated this website. Lots of new information: the Jape website was hijacked by a domain sitter (boo!) but we have a backup which you can reach; I've retired but am still active in research; I've applied (with Saeed Dehnadi and Benedict du Boulay) at Sussex for a research grant to follow up Saeed's thesis discovery of a major blockage in programming education.

I've retired!

I'm no longer employed at Middlesex. But I'm now Professor Emeritus (the Latin means "time served", nothing more!), so I've kept my email address and this web page.

What's New?

I submitted a paper to PODC 2012 on finding barriers in a work-stealing queue algorithm running on PowerPC. The latest version (with co-author Mike Dodds who showed me how to understand propagation effects logically) is here. A treatment of the LIFO version of the same algorithm is here, with a more careful logical argument, and my latest attempt to say what the logic I'm using is is here. This is work in progress: the concrete boots of soundness have not yet been tied to my feet.

Hasan Amjad and I published a couple of papers on Simpson and Harris's multi-slot shared variable algorithms first by brute force and then by refinement and linearisability. During the final stages of the refinement work we actually met Hugo Simpson, which was fun. But despite that, I don't want to think about his algorithm any more :-).

Saeed Dehnadi's work on predicting programming aptitude has led to a research proposal.

Jape continues to exist.


All the ones I've remembered to upload are here.


And slides are here and here.

Jape developments

Jape isn't dead, though I haven't made any changes recently. 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 continues to ensure that Jape is online. Domain sitters stole (blast them, and if you can find a way to warm their bottoms, be my guest). But we kept backups, and it is now here. Thanks Bernard. Bug reports to me, please, at any of my various email addresses (see above).

Jape is GPL licensed and the entire source is at sourceforge.

Feedback and bug reports to me, please, at the address at the top of this page.


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.

Ancient lectures, teaching notes and books

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.

Understanding and Writing Compilers

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.


Last modified: 29th Feb 2012 15:23:31 GMT by RB