Congratulations to Alexey Gotsman

Alexey Gotsman completed his PhD this week. Well done Alexey!

Healthcare reform article

An article in the Guardian by Bee: American healthcare is in truth already rationed

Congrats to Viktor Vafeiadis

Viktor Vafeiadis has won this year's SIGPLAN Doctoral Dissertation Award. Well done!

A new look at hardware synthesis

Check out the draft of a paper we've written on hardware synthesis.

See also: PPT slides that Satnam and I presented to Bill Gates.

Berkeley lectures

I'm visiting Berkeley University during the month of April. During my visit I'm giving 4 lectures on termination proving. Here are the slides. Warning: they're around 20mb each.

• Lecture 1
  
• Lecture 2
  
• Lecture 3
  
• Lecture 4
  

Roger Needham award

I won the Roger Needham award. Thanks to those who nominated me, the committee, and those who were asked to write letters.............whoever you are.

Interesting termination bug

Perhaps you heard about the Zune leap year bug? Sort of an interesting bug. This is a classic example of a liveness/termination bug, as explained here. And yes..... TERMINATOR can find this bug.....

SF weekly

SF Weekly makes note of the Vogue article.

Termination research now VERY fashionable ;-)

I'm mentioned in Vogue in an article about Tauba. Dec '08....the year termination research become fashionable ;-)

no kidding, functional programming has really arrived.....

Watching this talk gave me shivers. My love (functional programming) is now mainstream. Very funny talk, by the way.

Eric Koskinen

Welcome to Eric Koskinen, who just started his PhD at Cambridge University under the supervision of myself and Matthew Parkinson.

Professor Cook

Queen Mary, University of London has now appointed me as full professor of computer science. I'm not leaving Microsoft, of course, its a joint appointment with Microsoft Research.

methods of proving recursive programs terminating

I'll state this perhaps a bit too strongly (to make the point). Recursion, and program termination, are completely orthoginal issues. Check out our new paper: CFL-Termination. This paper shows you how (if you have an oracle for partial correctness semantics) you can convert recursive programs into semantically equiv. non-recursive programs without tricky encodings using heap or non-linear updates to arithmetic variables. Enjoy ;-)

F# release

Check out the community technology preview (i.e. pre-release of the "productized" version) of F#.

British pastimes...

cheers!