Latest Mac

Maybe this is what Steve Jobs didn't want to demo at MacWorld!

I'm a PC

I was reading some blog this morning and in the corner I noticed a familiar face on an advert.

Nordic Walking

On the advice of my Slovene physio, I had a training session of Nordic Walking last week on Parkers Piece.

Nordic Walking originates from cross-country skiiers wanting to practise during the Summer. The poles are much shorter than for skiing, but some of the same principles apply.

It's surprisingly easy to learn the (very) basics. It's an odd sensation when you're walking. You seem to walk slightly faster than normal, yet it feels easier than walking normally. (You put very little pressure on the sticks, so it is a little surprising.) The interesting fact is that you burn a lot more energy compared to standard walking (around 40% more). I'm doing it because it also forces you to equalize your stride - something that you *don't* do when you have an arthritic ankle:-(

So, if you see someone on Madingley Road looking like this, it's probably me. [When my daughters are teenagers, I might have to stop!]

Mapple

I want a Mapple!

[Thanks to Matt for the link.]

Dinner at Efes

We had a great dinner at Efes last night. We went with a crowd of friends from our neighbourhood. Lucy was there - who, impressively, is the only one of us with an entry in imdb! [She has a lovely voice.]

Britney Spears

Picture this. Britney Spears. Actually, Britney Spears in fishnet tights. More, Britney Spears in fishnet tights and black sequin hotpants. Something *exactly* like this:

Okay, now imagine all of this about 1 metre in front of you. Got that picture in your mind? Yes? Well you are now picturing what I was actually doing on Saturday night!!! Oh yes, oh yes, oh yes.

Mateja, Matt, Judith and I were in the audience for X-factor! We bid for the tickets at the Milton Road Auction of Promises that was held in the Summer to raise funds for the school. So I was that close to Britney "for charity" :-)

We had a fantastic time. It was fascinating to see how a live broadcast show is put together - the people are incredibly skillful, but things really are being arranged until 1-2 seconds before the cameras come back on! We had really great seats; here I am behind Danni's shoulder:

(You can just about make out my "I HEART BRITNEY" T-shirt!)

As we were guests of the producer we got to have a drink afterwards in the studio. I chatted with Diana - one of the contestants - she's a real sweetie. Mateja chatted with Eoghan. We ended the evening in the hotel bar chatting with Eoghan's Dad.

Alex Summers

Congratulations to Alex Summers whose PhD I examined with Hugo Herbelin at Imperial yesterday. Hugo and I (well, okay, mainly me) had lots of questions for Alex but he did a great job in answering them. His thesis addresses the question "what is the computational content of classical logic?" He looks at both sequent calculus and natural deduction formulations.

He has two very striking results. The first considers the question of adding ML-style polymorphism to classical logic. There are some old results from Harper et al. showing that this is non-trivial (i.e. unsound) but Alex shows that a proof theoretic approach can lead to sound answer. This is a very interesting result (we probably discussed this one result for an hour in the viva!).

The second striking result concerns his variant of the lambda-mu calculus. He derives a set of reduction rules that are able to simulate control operators with prompts. Until I read this I wouldn't have thought it possible. His calculus - the nu-lambda-mu calculus - is very elegant, and tidies up some of the loose ends that I tried to hide under the carpet when I was devising an operational theory for languages with control operators back in the nineties! If I had more time I'd probably go back to my old MFCS paper and see if the results would be improved by using a better calculus.

Anyway, Alex has some small changes to make but I'd expect his final version to be available soon. I recommend it to you!

Ona

Mateja's in the press again. I'm married to a media superstar :-)

Windows 7

Today, Austin gave us a trip report from PDC. As you may know, Microsoft demoed many things at PDC, including the successor to Vista, code-named Windows 7. Actually Austin gave the talk from a machine running Windows 7. I have to say that Windows 7 looks like a significant improvement on Vista. Aside from the eye candy (which is good too) it does seem that Windows 7 is both faster and smaller (it can target netbooks!). I'm really looking forward to playing with a beta!

[There's stuff on the web if you want to take a look. Here's some material on ZDNet. ]

Code

As I'm writing some code at the moment, it's nice to see that I'm not the only one who forgets to fix quick work-arounds!

Jazz Radiohead

Today The Guadian had an interesting article where they gave five jazz artists the Radiohead song "Nude" and asked them to make a recording of it. There are some interesting results. You can hear them here.

[If you don't have it already, the latest Radiohead album "In Rainbows" is, in my opinion, a work of genuis.]

Software services + DSU

I just read this note by Gilad Bracha. It's very nice (albeit a little light on concrete details). Gilad's aim is to consider an OO platform for software services, paying particular attention to the programming language perspective.

I was pleasantly surprised to see Gilad talking about dynamic software updating - indeed it's core to his proposal.

I had thought that our UpgradeJ paper would be the last thing I did on DSU (or rather the journal version - still in progress - would be). Maybe it was more prescient than we realized :-)

Check out Gilad's paper for yourself!

HTC Touch HD

Contrary to what I said a while ago, I reckon this will be my next phone. Nice.

[POSTSCRIPT: There's a nice review on The Register today.]

Ljubljana airport

I last flew through Ljubljana airport at least 5 years ago - maybe longer. It's been improved considerably since then. Most of these improvements are very nice - lots of steel, glass, nice chairs, a decent duty-free (where I got a bottle of viljamovka). The less-good improvement is the weird bus ride of 10m that you have to take after disembarking from the plane to get you to passport control.

I was amused by the glass "specimen cases" they have for smokers:

If you ever needed motivation to give up - I would have thought that being stared at by everyone else in the departures lounge would be pretty effective :-)

EasyJet vs Ryanair

I flew out to Ljubljana with the family (as it's also half-term). No great change there, but we flew to Ljubljana with EasyJet, instead of our usual flight to Graz/Klagenfurt with Ryanair.

I was surprised at how much more enjoyable flying with EasyJet is. Maybe it's just Ryanair setting a low bar, but it seemed like a much less stressful exercise. One crucial difference is that EasyJet pre-board families, whereas Ryanair makes them pay. I don't understand this - families need to be sat together and they slow things down. It just makes sense to get them on first. EasyJet appear to preboard their Speedy people first, then families, then everyone else.

In addition, they categorize "everyone else" into groups so they can manage the crush to get a seat. Ryanair basically encourages a free-for-all. This just brings out the worst in people. (I remember being pushed out of the way even though I had a leg in plaster and using crutches!)

I expect we'll be flying to Ljubljana in the future...

[The only downside of the trip is that I returned with a stomach-bug that has laid me low for most of today. I had to cancel my seminar at Oxford due this afternoon - I barely made it to the corner store this evening let alone a drive to Oxford :-( ]

Ljubljana visit

I'm back from a weekend visit to Ljubljana to visit Andrej Bauer and Melita Hajdinjak at the Maths Faculty. I'm privileged to be serving on Melita's thesis committee. I visited them to become acquainted with Melita's work. I was blown away: Melita has some very nice results. I'm encouraging Melita to submit some of her work for PODS...fingers crossed!

Car rental

I was a bit nervous at the Avis desk following my "Banana Yellow" rental last time, but I lucked out this time. I got a Chevrolet Impala LT, just like this:

It's a really nice ride.

Microsoft Surface

Whilst in Redmond I was housed on floor 4 of building 35. Luckily, just by the lifts on the fourth floor is a Microsoft Surface Computer. I congratulate the surface team, because this technology rocks! The demos they had running were very impressive. Ignoring the geek value of the games, I was particularly excited by the video and picture sorter. It really is like having the pictures scattered over the table - you can toss them around, resize them, even whilst the video is playing if its a video. It was a real immersive experience. The software seems rock solid. There were people playing with it most of the time, and it really does seem Just To Work (TM). Cool stuff.

Cultural difference

I'm just back from another great week "on campus" in Redmond. I was well-hosted by Jim and Erik. I've returned tired but excited about the work that we generated over the week - lots of new directions and ideas to try out!

There is a lot to blog about, but here's one of the interesting cultural differences I experienced on this trip: my first time at a drive-thru ATM (at Wells Fargo in Bellevue):

[Apologies for the blue-tint: somehow I screwed up the white-balance setting on my phone.] You can just about make out the car-door and the wing-mirror.

America really is the land of convenience!

Spore

Yesterday we had a talk from Ryan Ingram from EA about the use of concurrency in games software, specifically Spore. I'm not a computer games player, but I was *very* impressed with what he demoed. It's amazingly easy to create creatures, and they seem very characterful in terms of their animation.

Ryan's talk was interesting too: he discussed how games are increasingly taking advantage of multicore shared-memory machines, but also how difficult that can be. He showed some of the programming patterns they use, but he also pointed out how some things could be better supported by language design. I found this very interesting - there does seem to be a sweetspot for a practical language that has a constrained scattering of some POPL-esque language design features. if only I didn't have so much on already...

100% organic - evidence

I've promised a number of people a picture of the nail that was removed from my left leg. Here it is:

For scale, I placed a 30cm ruler below the nail (with two fixing screws). Yikes!

Old School

I like this website that shows what you can do with a ton of AJAX code :-)

Cambridge Graffiti

When I had my day off, I did notice a whole bunch of wacky graffiti around town. Here's an example:

Samso

I read an interesting article over the weekend (which was warm enough that one could read the paper in the garden in a deck-chair!). It's about an island in Denmark that has become completely carbon-neutral. In fact, it sells excess power back to the mainland. There are some beautiful photos too. [link]

Day out

At very short notice, I had to take a day off work today to look after my youngest. We had a very nice time: We had to get out of the house in the morning, so first we had a cappuccino and a "aquaccino" at Starbucks in Borders and some fun playing with some zoobs. We then went along to see the Roger Hilton exhibition at Kettle's Yard. Lina liked it: in particular the "running lady" as she put it [to the right here]. We then walked along the river home in time for lunch. Today was so beautiful, we went to Newnham Park after picking up Hana. A good day - although there's going to be a huge amount to do when I get to work on Monday!

Mike Hicks

I've blogged before about the large number of superstars that pass through MSRC. MSR has a visiting researcher programme where we host academics on sabbatical. Last year, I hosted James Noble - a by-product of which was a paper in ECOOP.

This year I'm thrilled to host the multi-talented Mike Hicks from the University of Maryland. He'll be here for three months, and then over the road at the University for a further nine visiting Peter Sewell. It's great to have Mike here - he's currently teaching me about dependent types and security policy. I expect to learn a lot in these three months!

Mike and his family are blogging about the experiences of living, working and schooling in the UK. I imagine it's all quite a shock for them! But his children seem to be settling in just fine - here they are in the Jesus Green Playground with Hana (Lina is off-camera trying to climb up on the highest slide for older children!):

Jerry

My professional and personal lives have just collided: Jerry Seinfeld stars in the latest Microsoft Ad (with Bill)! You can watch it here.

Surely in the next one they need a Microsoft Research angle...my agent is waiting for the call :-)

UPDATE: Episode two can be found here.

Chrome

We live in interesting times: Google has just released an open-source browser: Chrome.

I particularly like the fact that rather than write a boring white paper, they released a comicbook! That *is* a cool touch. [I confess the rather strong urge to start making my own comic...]

100% organic

A personal post: I've gone organic. But I mean this personally. *I* am now organic. For the past two years I have had a titanium intramedullary nail in my left tibia. On Friday last week, Mr Robinson removed it. (If you don't know what one looks like; mine looks like the one on the right here.) As Peter puts it: I have been de-bionic-ified.

Somehow I thought it wouldn't be too bad - but it turns out to be very painful :-( Naturally I was still at work the following Tuesday (Monday being a national holiday). Clearly I hadn't read this.

This area of medicine is a combination of high science and brute force: I love this sort of picture in a medical science journal article! It looks like something from a DIY store leaflet.

Bachelor days

I'm by myself at the moment, which gives me an opportunity to watch some episodes of Seinfeld (I have all 9 seasons on DVD - and Mateja doesn't like it). I had previously worked my way through to season 7.

Boy, has season 7 screwed up my plans of working in the evenings! It's genius. I thoroughly recommend it - you can get it yourself for a mere £13! This season seems more self-referential than others and the writing is all the more smarter for it. Moreover the season's story arc of George's wedding is a goldmine! Wonderful.

[ps: even though I'm a Seinfeld fan, none of my passwords are "Bosco", so try again hackers!]

Notepad goodie

I'm really an emacs user, but when you live in the Windows world (or maybe I mean the Microsoft world) the infamous "notepad" application ends up being a very convenient app to write little files. One thing I always hated about notepad is that when you fire it up, type in your two-line masterpiece and then save it always adds a ".txt" to the end of the filename you supply even if you had already given it an extension, e.g. you type fermat.sql then it saves it as fermat.sql.txt. Ug.

I just discovered a way around this - perhaps I'm the last person to learn this but... : if you type the filename with quotations notepad doesn't add the .txt. For example if you type "fermat.sql" then it really saves it as a .sql file. Hurrah!

The next laptop?

I'm a happy user of my Dell X1, but that's getting a little old-in-the tooth. I don't dare run Vista on it, but I have to run Office 2007/Visual Studio 2008 so combined with the usual cruft that one accumulates over the years it's getting very slooow!

Unfortunately it's not easy to find a lightweight laptop (around 1kg) with a decent screen resolution. (Oh, and running Windows, before someone suggests a MacBook Air :-))

Finally after months of rumours, Dell has announced a very nice new machine (here). Dual-core, SSD, 1kg, 1280x800 12.1" screen, and pretty cool looking too. No prices yet, so not sure what our IT manager will say...

The Catsters

Thanks to Nick for showing me what youtube was really meant for: Category Theory for the masses! Yep, the catsters have their own channel on youtube and you can improve your life by learning about adjunctions, monads, algebras, etc. Wonderful! Thanks, Eugenia.

What's next? Guerilla category theory?

Moshe Vardi talk

This morning I attended a magical talk by Moshe Vardi entitled "From Philosophical to Industrial Logics". This was a fantastic hour - Moshe gave a fascinating, historical tour of essentially a century of work on logic and automata. He showed how a number of seemingly esoteric academic arguments have been replayed in industrial situtations, e.g. the arguments between tense logic people on linear vs. branching time was played out between Intel and IBM when settling on the language PL/Sugar.

Moshe had some nice conclusions, including (paraphrased):

• science is a cathedral; we are the masons
• there is no architect
• our own contribution is always very small
• sometimes very small contributions can have a big effect

It was a really wonderful talk - I know we record these but we don't make them externally available. Someone should record this talk and put it on youtube or somewhere similar. I hope to get Byron to persuade Moshe to put the slides somewhere.

ECOOP talk

I've uploaded the slides from my talk on my webpage here.

[Attendees will be able to read the slides I had to skip :-( ]

ECOOP'08 day 3

Last night was the conference banquet. Whilst I had a good time, the local organizers took us to a big restaurant in Paphos Town. All fine, but we didn't get a separate room, but rather were sat in the same space as misc tourists. Again this would be fine, but ECOOP has a traditional of a banquet speech. This year the speaker is James Noble, and I was not alone in looking forward to his speech. (Those who know James will understand when I say that his speech could have gone in any direction!)

So James was made to give his speech when the band took a break and in front of all the tourists as well as us. This was really unfair, especially to James. The organization of ECOOP has been good - at least for me (although other people have niggles) - but this was a huge blunder IMO.

On to day three ...

Today started with a very interesting talk by Wolfgang de Meuter, who is this year's winner of the AITO Junior Award. He gave a talk on what he terms Ambient-oriented programming. What this means, as far as I can tell, is a form of distributed OO-programming. It's OO in the sense of Abadi-Cardelli-style objects (without the type system), and with mirror-based reflection. Wolfgang proposes a particular form of futures programming (and hence is heavily asynchronous - a good thing IMO). What was also interesting is that Wolfgang is a big fan of scheme, so he makes heavy use of closures.

It's probably worth looking up his language. I was trying to remember the section in the "C# joins" paper by Benton/Cardelli/Fournet where they code up futures in joins. I don't get the impression that Wolfgang is aware of much of the theory in distributed programming, so it would probably be worth figuring out where his work fits in the known literature.

The first technical session was interesting but let me mention Raymond Hu's excellent presentation about his work with Nobuku and Kohei on session programming in Java. Funnily enough I used to teach Raymond as an undergraduate at St John's College, Cambridge; so it's wonderful to see him doing first-class research, especially at my alma mater, Imperial College. Anyhow, in their work they have a simple session protocol language, and a session API, such that they can statically verify that the java code using the API adheres to the session protocol. Particularly impressive is that for their (admittedly micro-) benchmarks are very neat - they consistently out-perform Java RMI. Cool!

In the session after coffee Brian Chin gave a really nice talk about programming so-called "interactive applications" in Java. It turns out that there's a variant of the expression problem. He solved it some refactoring and actually implementing delimited continuations as a Java library. I want to take a look at this paper more carefully as I'm really interested to know how that can be done. Moreover it did occur to me that one might be able to do some of these rewrites with dynamic updates. Maybe.

After lunch we had the second talk of the day from Michael Ernst. He is an astonishingly good speaker - I need to learn from him. His second talk was way cool. He spoke about his immutability analysis for Java. It's a really nice analysis - it all boils down to graph reducibility. Their analysis is sound, complete, linear time, works for the whole of Java, deals with Generics,... wow!

ECOOP'08 finished with a very nice talk from Ewan Tempero on a study of the use of inheritance in a vast corpus of Java code. It does seem that most Java code uses quite a bit of inheritance, so perhaps some of the horror stories are not true! A good way to end ECOOP.

Now I get the rest of the day and tomorrow morning to relax in beautiful Paphos. Hurrah!

ECOOP'08 day 2

Day 2 started off with an invited talk from Akinori Yonezawa who is this year's winner of the AITO Senior Prize (last year's winner was my manager, Luca Cardelli). This talk was okay but a little disappointing in that Aki decided to give a "my research career in an hour" talk. It was kind of interesting, but naturally nothing was treated in depth. One big point was that his invention "concurrent objects" (interpreted VERY broadly) are used in Second Life. This is cool although it wasn't at all clear that the Linden guys did this knowingly; more that in a massively parallel world with objects - the objects have to migrate. Its obvious, so you do it.

I started off the next session with a talk on UpgradeJ. Unfortunately, this was not the best talk I've given - I ran behind schedule and didn't get my "5 minutes to go" warning, but rather only got the "1 minute to go" warning! Yikes. I had to skip quite a bit. Most of it was skippable, but I had to rush the description of evolution upgrades - which is a shame as it's the really interesting bit of the paper :-( Oh well. I have had a lot of questions through the day, so perhaps things aren't so bad. Sophia mentioned that she may try to get a project student to implement UpgradeJ which would be wonderful!

Donna Malayeri followed me with a sensational talk about combining structural and nominal types. I hadn't seen the ECOOP version, so I didn't know quite how expressive her system is. It's very nice indeed. She also got some of her dislike of Java out of her system - therapeutic I'm sure!

Anders Hessellund wrapped up our session with a neat talk about problems with real-world enterprise systems. It turns out that many of these systems are built with lots of XML "meta-data", and bits of Java that attempt to adhere to the meta-data, and provide BI. Of course, the way the Java code is produced is so horrible that it isn't checked that the code adheres to the design. Anders and Peter Sestoft have built some tools employing fairly simple data- and control-flow analyses to verify the code. Interestingly, there is some tension between precision and soundness. Given that they are dealing with real-world code they worry more about precision, so their analysis is both incomplete and unsound (but useful!).

After the coffee break, I went to Gilad Bracha's tutorial on Newspeak. I heard about this in FOOL in January, so there was a big overlap. But they seem to be making progress. Gilad did mention that they were interested in an optional "pluggable" type system (he put it thus: "It's a priority to us, just the lowest priority"!).

After lunch I went to the "hardcore theory session" (as someone mentioned over lunch). In particular I enjoyed listening to Anindya Banerjee talking about his work with David Naumann and Stan Rosenberg on their "regional logic". This is very nice. He motiviated their work using the subject-observer pattern. Their approach is very reminiscent of what Matthew and I did in our POPL'05 paper - using a set of observers, O, etc. However, they don't use separation logic, but rather effects and regions and some other operations. It's all very nice (they won a best paper award). However, I still think that the logical approach is more precise than using effects/regions. We need more experiments I guess.

Another great day. I'm off to grab a shower before the bus takes us to the conference banquet - should be fun!

ECOOP'08 day 1

The first day is over and what a day it was. I really enjoyed it.

We started off with Rachid Guerraoui talking about transactions. He gave a really nice talk - enough detail to make you think that maybe you should change research areas, and yet not too much to make you fall asleep (or check out the pool). The question he posed is whether we can just "inherit" all the stuff that Jim Gray et al. did in the 70s on transaction systems and just import them into our languages/systems and be done with it? Interestingly it doesn't seem so.

I had the honour of chairing the first session. Because of the welcomes and presentations before Rachid's talk we were already running 30mins late! To incentivize the speakers I offered an AITO Cypriot pear to the speakers who finished inside their 25mins slot:-) Fortunately the three speakers all rose to the challenge and got one of their five daily fruit+veg portions.

Nick Cameron kicked off with his wonderful work with Sophia and Erik on Wildcards aka existential types in Java. His presentation was very clear and it does seem that we finally have some understanding as to what these damn things are! As far as I know we still don't know if the system is decidable - maybe Andrew and Benli's work on variance could now be applied?

Jaroslav Sevnik followed up with a great talk on the Java Memory Model. It seems he really does have all the right tools in his hands to study this beast and he has managed to verify a number of useful transformations, and indentify erroneous ones too. Someone asked if he thought that Sun might rewrite the JMM. He thought they would but unfortunately there's nothing out there as a viable alternative. Sounds like a great PhD for someone with a huge brain! [My head hurts when I listen to the fine details of the JMM - like when Jaroslav gave a theory seminar in Cambridge :-( ]

Kathryn Gray rounded up session 1.0 with a very impressive talk about handling interop and inheritance between typed and untyped oo languages - she considered Java and Scheme as the languages in question. She did a really nice job about showing how the problem is perhaps more subtle than one might think, and her solution does seem pretty canonical.

All in all, I think people left session 1.0 ready for their coffee but glad that they stayed the course! [For some reason the timetable has 2.5 hours of talks before the first coffee break - Yikes!]

The rest of the day was of similarly high quality, but let me just flag Shan Shan Huang's talk on LiquidMetal, which was a very nice talk about the Lime compiler that takes a reasonably modest extension of Java and compiles either direct to the JVM or spits bits out for compilation on an FPGA and/or Cell processor. Really nice stuff - I need to talk with her about the fiddling that Satnam and I have done using LINQ.

A great first day. Now the nerves kick in for my presentation tomorrow morning...

ECOOP'08

I'm currently in Paphos, Cyprus attending ECOOP'08 and its associated workshops and symposia.

Firstly, it's an amazing venue. It's a nice hotel with several pools, beaches, and weather to match! Indeed, it's a pretty outrageous place for a conference. Normally the choice is between the talks and a natter with someone. Here the natter can be poolside, or you can just go poolside without the natter. It's a tough call. I've tried to be good and attend the talks I intended to, but I haven't exactly managed it (sorry Dino!).

There's been some interesting stuff so far. Susanne Cech Previtali gave an great talk about DSU and aspects - possibly the first time I could see a real argument for aspects! She had some very interesting case study data - I plan to steal some of it for my talk on Thursday. I also listened to Rich Hickey talk about his Clojure language. It's a lisp-like functional language for the JVM - so much like MLj (although I don't think he knows about that work), but it had some interesting features: primarily persistant data structures and support for concurrency. I don't quite understand how the immutability works in Clojure - esp. given the Java interop - but it seems worth chasing up.

I also went to Laurence Tratt's talk on programming languages. His point was that language designers need to think out of the box more and learn from other languages. That's kind of obvious, but the problem (not addressed) is that it's very easy to think you understand the essence of a feature by programming with it. Often language designers don't understand what they're doing - that's why we have so many, and that why many of them die.

The problem with Tratt's talk is that he didn't really seem to understand the area terribly well. Moreover, some of his conclusions were questionable (his criticism of checked exceptions was that people often put empty catch blocks.) I was tempted to ask him about my idea of licensing language designers (you only get a license if you have a PL PhD and can do all the exercises in Benli's book :-)).

In a little while I'm off to Dan Ingall's talk on Sun's Lively stuff, which I'm looking forward to.

Trailer

Tragic as it may be but I'm quite excited about the forthcoming film whose trailer appears here.

Make3D

I went to a really cool talk this morning. It was given by Ashutosh Saxena on his work on Make3D, which is a tool to generate 3d models from a (single) digital picture. Rather fashionably he uses machine learning techniques to build the tool. The results are pretty impressive. You can even upload images yourself to their website!

in rainbows in east london

LAST NIGHT\ SO GREAT

LAST NIG_HT SO GREAT

LA\ST NIGHT SO\GREAT

LAS_T NIGHT SO G_REAT

LAS\T NIGH\T SO GRE\AT

L_AST NIGHT_SO GREAT

Streets of Cambridge

One of the fun things about living in Cambridge (like many University cities) is that you get to see some unusual things. In fact, many "normal" things are probably quite unnormal elsewhere; e.g. walking my daughter to school (in of itself quite unnormal for many schools I guess) we are routinely passed by a chap on a unicycle. (My guess is that he works in the Science Park.)

Anyhow, seeing this on Chesterton Road on Friday afternoon prompted me to jump off my bike and take a snap with the phone.

Asus eee 901

There's a nice review of the new Asus eee 901 on The Register [here]. It seems that the concerns I had when I tried the 701 have been addressed, viz. better screen, and improved trackpad+buttons. However £319 is quite a bit of money as I was thinking of it as a laptop for the kids...

OCaml/F# vs SML

I've programmed in SML for many years. However, readers will know that recently I have been using F# quite seriously. I'm very impressed. It's really a very productive language. One minor problem for me are the subtle (syntactic) differences between the two. For example, I still find my fingers wanting to type [x,y,z] for lists instead of [x;y;z].

[I still don't get why people would want to drop the brackets around a tuple?! This is probably a hang-up from the pain that adding this feature caused me when I wrote the Imperial Hope Interpreter when I was an undergraduate! (Gosh - this was in 1990. Get over it!)]

Anyhow, I just stumbled across Adam Chlipala's OCAML/SML comparison page, which I enjoyed reading. [here] Check it out.

Dynamic Rebinding: journal paper finally out

The paper on dynamic rebinding with Peter, Mike, Gareth and Keith has finally appeared in Journal of Functional Programming (here). [You may or may not be able to view it for free from the JFP page - depends where you're reading it from.]

This is a great relief! Contained within are details of Gareth's mega-theorem (which proves equivalence between CBV lambda-calculus and our funky late-binding calculi (lambda-r and lambda-d)). Gareth sweated blood over these!

Enjoy!

Vista speed-up

Nick pointed me to Ed Bott's posts on ZDNet.com about some reasons why Vista appears so slow "out of the box". Ed took a brand-new Sony Viao and then spent an age removing the crapware that Sony put on the machine, and updating all the drivers (essentially by doing a fresh install of Vista). The result? A zippy machine. In Ed's words "...Vista doesn’t suck".

Looking at the ZDNet website, it seems that Ed has also included a number of other posts to help people "improve" their Vista experience.

ECOOP 2008: Early registration

If you're thinking of attending this year's ECOOP - and surely you are! - then you're running out of time. The deadline for early registration is June 1. You can register online here. It looks like a great program, and there's a whole bunch of interesting workshops.

The fact that the conference is in a beachside 5* hotel in Cyprus in July might just persuade you if you're still in doubt...

iPhone modification

Got an iPhone? Like to "improve" the UI? Here's the answer:-)

DBPL - Information Systems

A special edition of the journal Information Systems has just been released. It contains a selection of papers from DBPL'05. This edition was edited by myself and Christoph Koch.

It's been a long time in coming - but enjoy! There are some great papers.

Visited Countries

Visited Countries is a cute little web app where you select the countries you've visited and it generates a map - just like my one above.

New look live

http://www.live.com/ has changed its front page style. I think it's an improvement - what do you think? (I posted a while ago someone's thoughts on redesigning another well-known search engine's front page.)

Is it art?

I found these photographs by Li Wei amusing.

HTC Touch Diamond

Readers of this blog will recall that I'm a happy user of an HTC Touch Windows Mobile Phone.

Nick pointed me to this page with a teaser video for the new HTC Touch Diamond. Wow! In the absence of an iPhone with Active Sync, this looks like a really nice phone. These guys know how to tweak the Windows UI!

OOPSLA 08

Great news: Two papers by friends have just been accepted for publication at OOPSLA'08, which this year will be in Nashville, Tennessee.

1. Matthew and Dino's paper on JStar, which is their separation logic based tool for verifying Java programs.
2. Claudio's paper on his implementation of joins in the production Visual Basic Compiler.

Well done guys!

UpgradeJ available

Both long and short versions of our paper "UpgradeJ: Incremental typechecking for class upgrades" are now available from my publications page: here.

We'll be presenting this material at ECOOP 08 in July. If you haven't done so already, you can register here.

Rather amusingly/flatteringly, Alex Buckley mentions UpgradeJ on his blog (here).

Jim Gray Systems Lab

Microsoft has announced that it's to open a new, advanced development center in Madison, Wisconsin. The lab will focus on database systems and will be headed by David deWitt, who's joining Microsoft as a Technical Fellow. This is very exciting news! You can read the official announcement here.

Separation HQ

I've mentioned before the fact that we have hired some amazing people recently. It hasn't stopped. This week we welcome Samin Ishtiaq, who's joined as an RSDE working with Byron et al.

Samin worked on BI with David Pym and Peter O'Hearn and also wrote the paper "BI as an Assertion Language for Mutable Data Structures" (POPL 01) that laid much of the foundations for the current wealth of work in separation logic.

Cambridge (MSRC and UCAMCL) is now becoming one of the serious powerhouses for separation logic - use your favourite search engine to check out our work!

Expert F#

Today I just received my order from Amazon of a copy of "Expert F#" by Don Syme et al. I'm really looking forward to reading this. I'm now fiddling with F# every day - it's really a pleasure especially the Visual Studio integration and the interactive mode. Try the compiler; buy the book!

Eurostar

We went to visit our friends in Brussels for a long weekend. We decided to use this as an opportunity to try out the Eurostar for the first time - we've wanted to do this for years, but its recent relocation to St. Pancras made it especially attractive.

The main positive point is the convenience. We took the fast train from Cambridge and arrived in Kings Cross only 30mins before departure. It's a few minutes walk to the International Station. Check-in takes 10secs and the X-ray checks are very fast. Anyone who flies regularly will be amazed at how quick this can be. [We had the hassle that our 2 year old set off the alarm, and they were very rude about checking her. But I'm guessing we were just unlucky with the particular security person.]

The external area of St Pancras International is indeed very impressive. There has been a lot of positive press and I think it's deserved. I was somewhat surprised to find the rather sordid departures lounge past passport control (where you sit waiting to gain access to the platform). As far as I could see there was one cafe with a hundred people queuing for a coffee, one newsagent with thirty people queuing to buy coke because they didn't want to queue for a coffee, and a bar with ten people queuing to buy beer because they don't like coke (it was 07:45 after all). I was expecting more facilities. It does seem that they don't want you to turn up early.

The real disappointment was the train. Eurostar has been going for a while and the train was essentially original, i.e. it looked very dated, the carriage design is not great (no feeling of space), the chairs look quite shabby, etc. Indeed, as Mateja pointed out, the train from Cambridge was ten times better! The disappointment was compounded by the fact that even though I requested the seats to be together, they weren't. As our 2 year old doesn't get a seat, it was very cramped.

The convenience factor came to our rescue (a bit): it takes under two hours from London to Brussels. This is simply incredible. Given the lack of check-in time, and the fact that you arrive in the centre of town, Eurostar has an amazing advantage over the airlines. I'm not surprised that they've just turned in a profit for the first time!

Brussels is a slightly odd city, but rather than dwell on that, I'll just note that we went to two museums: (1) The Natural Science Museum. This has the biggest gallery of dinosaurs in Europe. We were a party with 6 children, and they loved it. Highly recommended. (2) The Royal Museum for Central Africa. A consequence of their colonial days, this was an interesting trip. They have deliberately kept the museum as it used to be, so it's not very whizzy, there's very little in English (only French and Flemish) and you can end up having some interesting conversations with a 5 year old about the evils of colonialism :-) Our kids liked it as we went to a safari park not so long ago, so they were keen to spot animals they had seen before. Particularly recommended is the cafe, which serves African food. We had an excellent Madagascan Chicken. Also impressive is the actual building it is housed in.

I have to confess to drinking a lot of Belgian beer over the four days. I really do like wheat beer - so I had a great time!

Now back to work onThe Big Secret Project...

File copying in Vista

I just came across this blog entry addressing file copying in Vista [SP1]: here. I can't say I follow it all yet but who would have thought that copying a file could be so complicated?! Nice blog entry though.

Life at Microsoft

One of the interesting things about visiting Redmond is seeing how different life is on the Redmond Campus and in the product teams. It's a little hard to explain but fortunately there are videos which show what life is like over there.

Sleepless in Cambridge

I'm now back from a wonderful trip to Redmond! I am grateful to Jim for being a great host. I met lots of people in Building 35 and learnt loads about TSQL. All very interesting. Now we have lots of work to be getting on with.

My fortune cookie at P.F. Changs read "You are wise to be deeply attached to your family and home". Maybe they know something about Microsoft that I don't but either way it's nice to be back :-)

Sleepy in Seattle

I'm currently in the Seattle area. I'm visiting the mothership and talking about The Next Big Project with various product people. All secret, but very exciting.

I spent today relaxing in downtown Seattle. I really like the Pike Place Market area: there are all sorts of people there; from dot-com millionaires to homeless people to ALT- people. There are funky places to have coffee and hang out. Next to a cheese factory I looked at some knives in a kitchen store that would have made Satnam cry had he been there!

The cool thing was somewhat spoilt by my rental car. Somewhat amusingly the woman at the Avis desk remembered me from my November visit. I thought I was polite but when I went to the car park I discovered that my Chevvy Cobalt was the lovely shade of "banana yellow"! Nice. [updated] See what you think:

Hmm...now off to get another coffee to get myself into the timezone :-)

iPhone with activesync

I'm a happy user of Windows Mobile 6. I've had some not-so-good phones in the past, although my latest - the HTC Touch - really is a nice piece of kit. My commitment with WM is because I really need my Outlook details on me at all times. (I used to use a PDA for this before I carried a mobile with me routinely.) I've tried other phones that claim that they can sync with outlook, but it never works.

Even though the iPhone is very tempting, I haven't succumb because I can't easily sync all my Outlook information to it. Somewhat amazingly, Nick pointed me to this interview with Terry Myerson [link]. It turns out that Microsoft has just done a deal with Apple to enable them to sync with exchange and embed active sync on the iPhone!!! Wow - I didn't see this coming! Once an iPhone appears with this feature I'll be first in line :-)

UpgradeJ

Despite having two PC members as authors, the paper on UpgradeJ by me, James and Matt got accepted for ECOOP08! We were a little surprised as one of the reviewers was sceptical - but I guess this is an example of author response working (there were others for ECOOP [putting on my PC hat]).

There were a lot of good suggestions from the referees so it'll take a while to fix. However we should be releasing a full version with proofs as a tech report at the same time we deliver the camera-ready copy. Hopefully next month. I'll post when it's available.

Anyhow - see you in Cyprus in July? (The perfect Summer location :-))

PS: Congratulations to James who got two papers accepted for ECOOP. (Doubly impressive as he had three submissions!)

Aero - no more

I've been resisting but...

...today my desktop was sooo slow. I was trying to show Claudio something in C# 3.0 but we had to wait a stupid time watching the animated wheel while Vista&VS fought with each other. I only have a single core machine but it is a 3.6Ghz Pentium 4 - not exactly a slow machine!

We went to the desktop properties and actually selected "optimize for performance". Essentially the machine reverted to a sub-Windows 2000 look - yikes! optimal? Maybe, but too embarrassing! So I've decided to switch off Aero and go to Vista Basic. Still looks okay and, it must be said, things are zipping along quite nicely. I have to wait for my multi-core desktop before I can do transparent windows again.

ECOOP PC meeting

I'm just back from two very exhausting days as part of the ECOOP PC that met on Thursday/Friday at Imperial College, London.

It was a very exciting but tiring couple of days. In the end we're going to have a great conference - we've accepted a really good selection of papers.

The process was very thorough - some papers were discussed for over 45 (heated) minutes! Jan did a wonderful job making sure that everyone who wanted to had a say. Moreover, we discussed many, many, many papers. We really needed two full days of arguing! (I had the good fortune of sitting between Kathleen Fisher and Doug Lea - so it was never dull!)

So, come to Cyprus in July! There's not only going to be a great programme, but you should definitely buy Jan a beer.

PS: MacBook Air count amongst the PC: 2

Hurrah for physical PC meetings!

Environmentally friendly they are not, but there are advantages to physical PC meetings. Thursday and Friday is the PC meeting for ECOOP 2008. (I'm also on the PC.) By the good fortunate of being close to London, I managed to persuade William Cook to visit MSRC. It's been a fascinating three days - thanks for coming William!

In addition we have had Kathleen Fisher, Bob Gruber and Erez Petrank visit and give great talks. Yesterday, James Noble popped by and on Monday, Robbie Findler will visit and give a talk.

It pays to be close to Imperial!

(I'm looking forward to the ECOOP PC meeting - I'll post my impressions...)

MacBook Air

Matthew came to my office on Monday and broke an important rule: Former PhD students are never allowed to have better laptops than their supervisors!

Yes, Matt brought his MacBook Air with 64G SSD. Here it is on my desk next to my less sexy Dell desktop:

My impression: It's gorgeous! What impressed me is not the weight, indeed my trusty Dell X1 is lighter, but the fact that it feels like a serious laptop. It's not plastic, it doesn't flex and I don't need to sharpen my fingers to use it.

It's beautifully designed. I take the criticism that one USB socket is a limit. I'm not so sure about the non-removable battery issue. I swapped in the heavier battery in my X1 when I got it, and I've never swapped it out. At least for me, the fixed battery wouldn't be a problem.

I'm still not happy that Matt has one and I don't though :-)

Othello @ Donmar Warehouse

Thanks to my wonderful brother, Mateja and I went to see the last performance of Othello at the Donmar Warehouse. This production has been highly praised ("An Othello for our times" - The Guardian), but even this didn't prepare me for the show!

This was the most amazing show I have ever seen. There was nothing to fault. From the lighting to the sound to the music to the minor characters, it was suberb. However, above all Chiwetel Ejiofor totally commanded the stage. His power was awesome, and yet he gave the part great subtlety. The scenes with Ewan McGregor (Iago) in the second half were particularly wonderful. I'm sure people will speak of this Othello in years to come.

There have been some criticisms of Ewan's performance - essentially that it was too weak and not sinister enough. However, I think they miss the point - I think Ewan was trying to give the audience some reason for *why* Iago was trusted so utterly by both Othello and Emilia. Were he such a cartoon villian surely someone would be suspicious.

At the end of the performance there was a notable pause before the standing ovation - people were so shocked. A woman a few seats away from me was in tears. Even afterwards, we found it quite hard to talk after the show. To be exposed to that much emotion and tragedy takes it out on you! It's amazing to think that this play was written four hundred and five years ago - but I'm sure this sort of performance was what Shakespeare had in mind (or, perhaps, even better that what he had in mind).

Photosynth video

You've got to watch this cool demo of Photosynth and other cool graphics apps from Microsoft: here!

[Thanks to Nick for the link.]

Ted Nelson in Cambridge

Ted Nelson - the inventor of the term hypertext, amongst other terms - was in Cambridge today giving a seminar at the University Computer Laboratory.

I enjoyed his talk. It was deliberately provocative, and perhaps not even Ted believed all of it. But definitely worth hearing and thinking about.

Ted's main point was that most modern computer systems (both the OS and the applications) today are essentially the same as was defined in the 1970s on UNIX. That time (the birth of UNIX) represented a moment (perhaps the only one we'll have) to break free of certain concepts. He discussed paper - and how it is a constraining medium for information - look at all the funny notation that copy editors and others have for denoting meta-information. Look at the problems people had in versioning paper documents. None of this is easy with paper and we knew these problems. So in 1970 we had an opportunity to re-invent the document. But we didn't. We still essentially imitate the paper format. [And lots of other weird restrictions - why is a document a single file?] As Ted put it: WYSIWYG is just propoganda for paper simulation. (Or better: doing this is the equivalent of taking a 747, ripping off the wings, crippling the engine and using it as a bus). As HTML contains embedded markup (and only one-way links), Ted classifies it as an "unmitigated disaster"!

He demonstrated the Xanadu Space application, which tries to offer a fresh look at documents. It looked quite nice, although not terribly novel (I've see similar apps for photo management for example).

He also described design in computer applications by considering the representation of time. We tend to show it using a circle for the hours and a table for the calendar. He pointed out that we should really unify these views and represent time as a spiral. He also made the following point, which is really quite beautiful:

The aim of any user interface is mental clarity

He wrapped up his talk by discussing very briefly his generalization of data structures: hyperthogonal cell constructions. This was quite nice, although I didn't agree with all of his criticisms of relational databases. First of all, Codd's vision was relations, not tables. Second, whilst we accept that tables are an artifical construction they allow us to build expressive query languages and execute them (very) efficiently. It's a trade off. Ted didn't mention any programmatic querying of his data structures - but I'd be interested to see if there was anything plausible here.

Anyhow, a fun talk.

For the interested: An entry on Ted on wikipedia is here.

MSR-NE

Microsoft Research has just announced a new research lab: Microsoft Research North East, to be based in the other Cambridge. Good luck to Jennifer and Christian!

Asus Eee

Thanks to my colleague Dinan, I've been able to spend the evening playing with the hottest laptop. No, not a Macbook Air; but an Asus Eee. In case anyone reading this isn't a Geek: the Eee is an ultra-lightweight Linux laptop. It weighs 920g and has 4GB Flash rather than a hard disk. Incredibly it costs 219pounds! Amazing.

Having fiddled with it, I'm pretty impressed. The keyboard is really pretty small, but as I'm not a touch typist it has proved reasonably easy to get used to. I wouldn't want to write my next POPL paper on it - but it's perfectly good for writing blog entries (this one!).

The screen is a little low resolution and small, so the surfing experience is dependent on the website being visited. For example, the bbc.co.uk website beautifully resizes itself, but others (that I shan't mention) are less pleasant.

As this laptop runs Linux, it uses Firefox. I haven't used this browser before but its pretty good. I tried youtube and my daughter tried cbeebies, so I can safely say that the flash support works!

All in, this is a really nice machine. There is an obvious trade-off: If you want small then you can either pay serious money for a full-powered machine - like the Sony TZ range, or Toshiba R500 - or you pay little and get compromises. As compromises go, this is pretty impressive. You just can't argue with 220 pounds! As a little machine for blogging, or a machine for kids to surf - this is fantastic! If I found an extra 1500 pounds down the back of the sofa, Id buy a Sony TZ31.

V2.0 of the Eee ought to have (i) a bigger screen/higher resolution, and (ii) better battery life.

Slovenka Leta 2.0

For those of you who want photos and videos; there are some on the 24ur website (all in Slovene).

Here's a photo of Mateja with Danilo Turk, the President of Slovenia:

MSRC postdoc positions available!

We are hiring post-docs - two year research positions. The closing date for applications is March 1, 2008; see here for details.

Our group is looking for top-notch researchers in programming languages, tools, and security. If you would like to make informal enquiries, feel free to send me (or one of the other researchers) an email.

Ljubljana

Our night in Ljubljana reminded me that it really is the best capital city in the world! We left the theatre and following Ivana's suggestion, we walked maybe 200m to Dabuda (which I discovered has a website here). It was a great place - funky decoration, beautiful people, fantastic cocktails, with a buzzing atmosphere but not stupidly busy and not ridiculously expensive! Perfect.

Certainly I can't imagine anywhere in Cambridge that cool, and anywhere in London would require a second mortgage (it cost 38Euro for 8 cocktails). The thing about Ljubljana is that if we had walked another 200m we'd have found another similarly great place.

Maybe I can persuade MSR to set up MSR-L :-)

Slovenka Leta

As I posted before, Mateja was nominated for Slovene Woman of the Year. We have just come back from attending the awards ceremony in the national theatre in Ljubljana ("Ljubljanska Drama").

We had a fantastic time! It wasn't quite what I expected: the "ceremony" was preceeded by essentially a variety show. Some of Slovenia's big names in music and comedy performed, so it was a very special evening for all Mateja's family (on top of being very proud of Mateja). Mateja looked particularly stunning in her dress designed by Stanka Blatnik.

In the end, the award was won by Lilijana Kornhauser Cerar - who's a pediatrician and head of the infant care unit at Ljubljana hospital. A very worthy winner.

After we met up with Mateja, we went to a reception and had a fantastic time - lots of champagne and probably not enough food to soak it up. "Team Mateja" (Mateja, me, Dragica, Zvonko, Primoz, Jana, Maja, Jan and Ivana) decided that having drunk that place dry, we were ready for more, so we went for cocktails at a very nice Restaurant/Bar, Dabuda. We had a really fun time here before staggering back to the car and back to Slovenj Gradec.

This was a very special night - we're all very proud of Mateja (especially me!). Oh, did I mention how stunning she looked?...

Postscript: Claudio found an article in English here.

post-POPL: FOOL

After POPL I also attended FOOL - which is a workshop I really enjoy. Excellent people come and there is always a friendly atmosphere. As there are no proceedings, people present quite preliminary ideas. You often see them appear at the next POPL/ECOOP/OOPSLA - so the quality is high.

After the night before (see previous posting) I was in need of a big breakfast. Luckily the paracetamol kicked in quickly enough that I was in shape for the first invited lecture by Jeremy Siek. He spoke about gradual typing. I had browsed this stuff before and hadn't paid it much attention. Jeremy gave a great talk - I now understand what this stuff is trying to do. It's actually quite nice. He spoke at FOOL about combining it with type inference a la Hindley-Milner. He has some nice results, although I couldn't see how it would work with subtyping though.

The other invited talk was by Gilad Bracha, who's at Cadence (no longer Mr Java!). This was a typical Gilad talk: full of neat ideas, inside jokes and self-deprecation. He spoke about Newspeak, which is a Smalltalk/Self-like language they are developing at Cadence. He demonstrated the language by considering parser combinations. They come out very nicely in Newspeak. He also demo-ed the language environment on his Mac.

Unfortunately I had to leave FOOL early to catch my flight back to London. All in: this was a great trip. The POPL programme was excellent I thought, and it was organized very well. The only grumble was the internet connectivity but this is a common problem at (non-networking) conferences. It seems to be a problem that requires a large sum of money to solve :-(

POPL day 3

The final day of POPL started with an invited by Yaron Minsky from Jane Street Capital, who are a trading company based in Wall Street. The moral of his talk was that Jane Street's language of choice is OCAML. His talk was very interesting - indeed there was some discussion at the end as to whether it could be taped - it really should be seen by undergraduates! In some senses he was preaching to the converted (Functional Programming is A Good Idea!), but it was very nice to hear it explained so convincingly.

Yaron listed Jane Street's technical requirements for code: (1) Correctness (2) Agility and (3) Performance. When you are trading millions of dollars, correctness of code is very important! Indeed, the partners of Jane Street code review *all* the code. For them, the clearer the code the better. In addition, succinctness is important. That helps Jane Street be agile in their development, as does the expressiveness of OCAML. Finally, OCAML's efficient compilation is very important. During peaks in the day, Jane Street can be dealing with 100,000 equity transactions a second, and recording .5TB of data a day. This would not be possible unless OCAML were efficient.

A couple of other interesting facts from his talk:

1. They tried C# before moving to OCAML. They dropped C# because of code verbosity and the difficulty of reasoning about their code.
2. He mentioned that they hardly use the objects features of OCAML at all.

The rest of the day was packed with great talks - it was hard to find time to sneak out and buy presents for my daughters :-) Some highlights for me:

• Conor McBride's talk was fantastic. It was typically eccentric - but Conor was even more on fire than normal. He had good jokes and he's really cracked animation via sellotaped ohp-slides! He was talking about some funky zipper-like techniques for walking over tree-like data structures.
• Hugo Herbelin got me all nostalgic again for lambda-mu-calculi. I wrote a paper a long time ago about operational reasoning in a lambda-mu version of PCF. No-one has ever read this paper - which is a shame as it contains some nice results. (IMHO it's more slick than the Ong-Stewart treatment, but that still gets lots of citations...) Anyhow, Hugo gave a nice talk about generalizing this calculus (or rather the "tp" variant) to delimited continuations. Nice stuff. Maybe I'll revisit this area...
• Sam Tobin-Hochstadt gave a wonderful talk about Typed Scheme. I've been thinking about this problem for a while - so this is the paper I am most itching to read when I get back to Cambridge.
• Nate Foster gave a cool talk about Boomerang, which is the UPenn programming language based on lenses.

To celebrate the end of POPL, Matt and I tried the hotel's signature "flight of martinis". This is a little tray of three small cocktails. This is a very nice idea, as you get to decide which full-sized one(s) you want to drink. In between cocktails we went for a fun Chinese at Brandy Ho's in Chinatown. Brandy knows her fish - thanks to Dana and Christian for ordering for the whole table! We went back to the hotel for cocktails and then after a while I realized that I was keeping up with Matthew and it was getting late. Not a great idea, so I bailed out and staggered up to my room leaving Matt drinking until the early hours :-)

POPL day 2

The highlight of the day for me (and with the greatest respect to the other speakers) was Ken McMillan's invited lecture. Wow - this was one of the best invited talks I've been to! Ken explained the notion of "relevance heuristics" in program analysis.

He started by considering abstractly one of the key tensions faced by program analyses: the tension between precision on the one hand and scalability on the other. For example, imagine we have two facts at some merge point. In analyses based on least fixed points we typically lose information at merge points (a loss of precision); in analyses based on predicate abstraction we form a disjunction (which is precise but does not scale). Can we do better?

His insight is to be inspired by techniques used by modern SAT solvers. They exhibit a form of laziness in that they only resolve clauses when model search fails and they also learn from the past. [And lots more!]

Ken then showed how these techniques can be adapted to program analysis: one of the key tools is a use of Craig's interpolation lemma in the refinement process.

What was most impressive about the talk was that it really captured the entire audience's attention. Peanut-brained researchers like me followed the start and could see what was happening in the later parts, but also the real experts in the room (Tom Ball, Byron, ...) all seemed to be concentrating hard as the material got tough too. To keep everyone happy is a real achievement.

Thanks, Ken.

The day finished with a very nice meal at Cafe Kati - a Cal-Asian restaurant (hadn't heard of that before) - with Peter, Matt, Mike and Alex.

POPL day 1

The day started off with a very slick invited lecture by Walter Fontana on systems biology. [It was preceded by Phil Wadler suffering a "Janet Jackson moment": he tried to rip open his top to reveal his lambda-superman T-shirt, only for the zip to get stuck!] He made the interesting observation that the key notions that enabled modern chemistry can be seen as rules, instances and event. His assertion was that the same features were enabling systems biology. He also discussed the use of various abstract interpretation techniques. One example is in "pathway discovery". All in, a very nice lecture.

The talk by Aydemir et al was very interesting - in particular I liked their locally nameless representation of terms and cofinite quantification of free variable names. This is very slick.

Iulian Neamtiu gave a beautiful talk of a new "contextual" effect system that allows better timing of updates for dynamic update systems. I wish we had thought of this when we were developing our DSU stuff!

There followed a couple of really nice talks providing (operational) semantics for languages with transactions: one by Moore/Grossman and one by Abadi et al. Both seemed entirely reasonable - I think a sign of them representing the right choice rather than the problem being easy! The two approaches made quite different assumptions but I had the feeling that their essence was related.

The session after lunch was on separation logic. I'm biased - but Matt did a really great job presenting our paper! Christina David also presented her work very clearly. [This work, whilst completely independent, makes very similar contributions to ours: primarily, the use of static and dynamic specifications for methods.] James Brotherston wrapped up the session with his recent application of his cyclic proof structures to separation logic. This stuff gets more attractive the more I hear it - I'll have to read his thesis...

The excitment of getting a network connection meant that I skipped the final session to catch up with email and natter with various people.

The day wrapped up with me, Peter, Christian and Matt eating obscenely large steaks and washing it down with an agreeable Zinfandel at Alfred's Steakhouse.