Jo in the USA

Congratulations to our artist friend, Jo, whose work is being exhibited at the Agora Gallery in New York next month. (We have one of her more abstract pieces up on our living room wall.)

Virgin

The Heathrow-DC part of my POPL was on Virgin. It was my first time on Virgin for a transatlantic flight (I always fly BA to Seattle). It wasn't that good. However, it wasn't quite this bad.

Who's that guy?

I discovered that one of the advantages of flying through DC is that you can bump into some interesting characters.

post-POPL: PLAN-X

The day after POPL offered three very good workshops: TLDI, FOOL and PLAN-X. I had the great honour of co-chairing PLAN-X with Alin Deutsch. [Alin has done some fantastic work, so it was nice to finally meet him having followed his work for years!]

Given the competition for audience (esp. as TLDI is biennial), PLAN-X was a scaled-back affair this year, but I think the meeting itself was very good. I was really impressed with the work presented, the talks, and the audience participation. Every talk got good questions, and there seemed to be conversations carrying on over the coffee breaks too.

Some personal highlights were:

• I was delighted that James Cheney agreed to give the keynote. He's doing some interesting work applying PL techniques to reason about various forms of provenance in e-science databases. I like what he's been doing, although I wonder if recent techniques being developed by my colleague Nick Benton might be useful. I should just roll up my sleeves and get on with it.
• Curtis Dyerson gave a great talk on defining a shape polymorphic query language XML. The interesting thing is that he was "inspired" by Barry Jay's work; but they seem to have ended up with something different. At the moment, the connections with Barry's work (soon to be published by Springer - well done, Barry!) are unclear. I'd love to see that sorted out.
• Patrick Michel gave an interesting talk about verification of data-centric applications that process XML with fixed schema, and in particular verifying integrity and value constraints. They have an interesting specification language and it turns out that after some clever rewriting, a weakest precondition property can be derived. This is related to our work on M, so I'm going to dig deeper here.
• Ryosuke Sato presented some nice work on stream processing of XML-like data. The problem is trying to automatically translate tree-processing code into stream-processing code. It turns out that earlier work by Suenaga et al. used a type-based translation using ordered linear types. However, sometimes this results in inefficient buffering of data. The neat trick presented here is a variant translation that uses ordered (non-linear) types as well.
• Hiroyasu Nishimyama, in addition to having the coolest netbook of the whole of the POPL audience (an earlier version of this one), gave a nice talk about speeding up processing of XML by optimizing the parser given data from an earlier pre-analysis of XML data. This pre-analysis searched for frequent patterns in the documents. In more systems-oriented uses of XML this turns out to be very common, so they get big speed-ups in processing times.

(I liked all the other talks too, but these were the ones closest to my own research interests.)

I ended up having dinner with Nick, Andrew, Peter, Scott, Susmit, Tom, Xavier at 45 Bistro (again). I had the beef carpaccio followed by the filet. An excellent way to end the extended POPL trip!

POPL'09: day three

Today kicked off with a keynote from my old friend, Alex Simpson, who spoke on "linear types for computational effects". I *really* enjoyed Alex's talk - but there again, I did write my thesis on linear types, and spent a couple of years on a postdoc position trying to doing something similar :-)

Alex has, I think, actually solved the problem that we were trying to sort out but too dim to make any serious progress, i.e. a universal metalanguage for cbv and cbn. In those days we hoped "pure" linear types would suffice. They don't quite work. What Alex has now done is figured out which bit of them you need.

Alex starts with not the computational lambda calculus, but an interesting variant: Filinski's effect calculus. This makes a similar distinction of value and computation, but actually has two grammars of types. Alex then "enriches" the calculus with linear types, but does this using a Girardian "stoup". A really nice feature is that Alex has a decent, computational explanation of the stoup: a term with a stoup is an evaluation context, i.e. it's a linear function that "immediately" evaluates the computation that is put in the hole. [As an aside: Andy Pitts and I had fiddled with evaluation contexts and Lily; for a while we had an evaluation relation that internalized the evaluation context using linear functions. Very cool, but too confusing so we dropped it.]

Anyhow, Alex has a very natural calculus whose induced monad is commutative - the big problem with early linear work was that the induced monad was non-commutative. As there are very few non-commutative monads, this was a very sore point.

So, I really liked Alex's talk - I think there's some very nice more operational work to be done here. I shall be waiting for Alex to publish his slides next week - maybe I'll end up taking a trip to Edinburgh sometime soon...

I then enjoyed three talks on program logics. Nearest to my heart was James Brotherston's talk on a classical version of BI. It's highly non-trivial to find a classical version of BI that doesn't collapse everything, so it was sweet to see it all work out.

I also enjoyed Benoit's talk on open existential types. Essentially they have deconstructed the existential operators, so (in my view) they are more like module-like operators. However, the resulting calculus is (also in my view) much simpler than any module calculus I have seen. Benoit rushed through some of the details, so I look forward to checking this paper out.

Neel did a great job describing his work on focusing and pattern matching, especially as he faced not one but two laptop crashes in his talk. Poor guy.

POPL ended with a great talk by Chris Hawblitzel. Chris has implemented a couple of garbage collectors in BoogiePL; had then verified by the Boogie/Z3 infrastructure, and then he has spliced them into the Bartok compiler. Wow! You wouldn't have thought it possible - so this was a nice way to end POPL.

I ended up having a nice walk along the river with Lars and Alin (after we were stood up by Andrew and Claudio!). We went for a beer at one of the many bars and then had a nice meal at one of the "Italian" restaurants (Calamari followed by rack of veal). [Unfortunately I think the chap who was sneezing over me in PLPV has passed on his bug, so I had to go to bed early and have a bad night's sleep :-(]

POPL'09: day two

Another great day at POPL; although I - like the other MS people here - had my mind partly on other matters.

The day started with a wonderful talk from Chris Barker, from NYU. Chris is a linguist, but he uses ideas from functional programming. He made the interesting point that language also has a notion of side-effect, e.g. compare "john left the room" and "that idiot John left room". The phrase "that idiot" has had a side-effect on the semantics of the statement.

The heart of his talk is the fact that some constructions in language provide their own context, e.g. "John and Anna read the SAME book". Providing a meaning to SAME requires same to access the context, or in other words the continuation.Chris went on to propose a delimited control operator that could be used to give a semantics to SAME. This is a rather unusual control operator as it operates wrt another control operator. Moreover, as someone pointed out in the questions session, there is some ambiguity in the reduction. Chris made the insightful response that PL people struggle to remove ambiguity, whether NL is *full* of ambiguity!

That said, the PL coommunity should be talking more with the NL community, so this invited talk did a lot of good. Talking with people at lunch, everyone seemed very impressed with Chris' talk - so perhaps this will happen. Great talk, Chris.

I then listened to a great talk by Ronald Garcia, who managed to show how to simulate lazy evaluation in a CBV language with delimited control. This was VERY interesting - I think it's pretty surprising that it work. Indeed, Matthias seemed surprised and impressed. I need to read the details of this work.

I then went on a monster coercion-paper-thinking session with Nik. Two hours before and two hours after lunch. The good news is that I think we're finally getting somewhere thinking about polymorphism. [It also shows how much better it is to work with people in the room, rather than on the other end of an internet connection.] Maybe we will make the ICFP deadline after all...

I heard a great talk by Ross Tate about an optimization strategy where they actually don't rewrite the original program, but somehow store all the possible rewrites and then pass a cost function at the end to extract the final optimized program. This is something I've been wondering about for ages, as this is what database query optimizers do. I'm really excited to see someone formalizing this. I'm hoping to talk with Ross to see if they've considered the connection with database query optimization. I'd love to work on this myself.

I never miss a talk by Dino DiStefano if possible, and today was no exception. He gave a great talk about how they use a new notion of abduction to synthesize invariants for their space invader project. Dino's work is always very impressive: today it ranged from logic, to running the prototype over the entire linux kernel and showing the running times! Coolness.

Four of us M'Softies went for a stroll and then had a couple of cocktails to drown our sorrows. This was a great idea until we tried standing afterwards. Yikes! Jen's martinis are frightening strong it seems. We then went back to the hotel, met up with some more people and then went back to 45 Bistro. I had a spectacularly good meal with Nick [who uncharacteristically left early!], Thomas and Jens. (I strongly recommend the crab cake and osso bucco. Both were probably the best I've ever had.)

POPL'09: day one

A really nice day to kick off POPL.

[BTW: MSR has nine papers and one invited talk at POPL!]

The conference started with my colleague, Tim Harris, giving the first keynote talk on language support for TM. As with all of Tim's talks, it was beautifully constructed and presented. The big picture is that Tim suggests that atomic blocks should be separated from transactional memory, i.e. they should be treated much more abstractly than they often are. I have to confess that I felt a little inadequate during the talk. Tim navigated the design space during the talk, and I just don't know enough about the choices and the consequences to really follow what Tim was saying, why some approaches make more sense than others, etc. Of course, this gives me something to talk about with Tim back in Cambridge!

Alexey gave a great talk about his work with Byron, Matt and Viktor on reasoning about non-blocking algorithms. I also enjoyed Martin's talk about co-operative threading. He had a very nice model, with very clear operational and denotational semantics (that's fully abstract).

Dana spoke about static contract checking for Haskell. She did a great job of the talk, although I confess to being a little confused. She seemed to be doing a symbolic evaluation (using call-by-name) of contracts written in Haskell (call-by-need). Hmmm...

I then heard about masked types which is an approach to avoiding the brutal "default initialization" technique employed by Java/C# to prevent access of uninitialized fields. This was quite nice - it reminded me of the work that Matt and I did on Java effects. (Although I don't quite know why Xin thinks the Java/C# approach is "unsound" - ugly, perhaps, but not unsound.)

Daan rounded off the morning with a really neat talk about his latest work on first-class polymorphism. Daan gets better and better about describing this stuff. He even survived some barbs from Karl on type inference :-)

I had a very jolly lunch, chatting with Donna, Matthias and Shane.

Later my colleague, Nikhil Swamy did an amazing job, giving a talk on SPEED - which is a tool that estimates the computational complexity of C programs - on behalf of the authors, none of whom could make the conference.

I really enjoyed the panel on "Grand challenges for programming languages".

• Simon Peyton Jones suggested the topic of controlling effects.
• Xavier Leroy emphasized the importance of verification; in particular what he referred to as "end-to-end verification".
• Unfortunately, Martin Rinard couldnt make it, but Arvind showed us his slides and did a great job of presenting them. Martin was typically outrageous - "all software is overengineered" - and suggested that we need to pay less attention to perfection in software. Beyond the obvious shock, I think that Martin's point is a good one. Really we need to figure out how to combine perfect and imperfect software and to keep them separated. Actually this was behind our work on UpgradeJ - we wanted to be able to write code that, e.g. call a method directly unless it is version n in which case we do something else...
• Kathryn McKinley made some nice criticisms of transactions (they lack decent communication). She encouraged us to look again at some of the ideas in high-performance fortran.
• Greg Morrisett encouraged us to work with architecture people - this area must change, and we have lots of expertise that we could apply to the problem of designing the next generation of computer architecture. (For example: what will the next generation instruction set look like? This is as much a language issue as an architecture question.) He also mentioned three supplementary issues: (1) How do we program the coming world of lots of robots (including biological robots); (2) The gap between PL and HCI worlds needs reducing; and (3) We need to think more about education. (For example, we have no standard textbook - hence no unified voice)

I then went for "shrimps and grits" with Peter, Francesco and Suresh. We spent much of this time trying to understand some of the aspects of Tim's keynote. I think we understand it a little better now...:-)

Anyhow, a nice start to POPL.

pre-POPL: PLPV

I attended the workshop on "Programming languages meet program verification" on the day before POPL. There were a whole bunch of interesting meetings on the same day, so it was a tough choice, but it turned out to be a good choice.

The invited lecture was given by Manuel Fahndrich from MSR in Redmond. The talk added to my already high opinion of Manuel - it was really wonderful. He described his post-Spec# work :-) Rather than extend the language, his idea is to provide a very simple Contract class, by which the code can specified. The specifications are written in the programming language itself, e.g. Contract.Requires(e) and Contract.Ensures(e), where e is a C# expression. (His examples were in C#, but he also showed some code in VB. The recent extensions in VS 2008, such as lambda expressions, help here.) The code is then compiled to, in this case, MSIL. It's at this point that Manuel's tool kicks in, which then goes to work on the IL code, figuring out where the pre- and post- conditions are; reconstructing the expressions and then either performing a static check on them, or baking in the assertions so they occur at run-time. Also interesting was that he did the static checking using abstract interpretation rather than using a theorem prover, as in Spec#.

This was very nice. The real advantage is that they haven't extended the language at all, so they don't have to invest any time in compiler work, tools, etc. and they can concentrate their efforts on the MSIL munging. The other advantage is that MSIL is a common intermediate language, so this could work for other .NET languages, eg. VB, C++. All of these techniques could work for JVM-based languages too.

I left this talk wondering whether Matt and I ought to think about this wrt our work on separation logic. One of the possible weak-links in Manuel's work is that they have an unsound heap abstraction, also they have a rather naive handling of inheritance. Another thing that needs doing is seeing whether Manuel's techniques would work for F#. The MSIL emitted by the F# compiler is quite different to the sort emitted by C#. So I suspect they'd need to do some work with their analysis to handle this. The hope might be that things will get easier, as there should be less state-minging code. Moreover, the F# emits highly predictable MSIL code (a fact it took me ages to realize and appreciate this - I now think it's a master-stroke by Don) which would also help their tool. too many ideas, too little time...

We then had two CMU-type-theory-talks in a row :-) The type-theory du jour at CMU right now seems to be polarized type theory. I heard some of this when Bob Harper was visiting MSRC, although I was a little rusty during the talks :-( Anyhow it seems that this type theory can give a fresh insight into problems with union types, and the value restriction. This seems very nice - I've blogged before about Alex Summer's PhD that has another account for the value restriction wrt callcc. I was left wondering what the connection might be.

Kenn Knowles then spoke about some improvements to simplistic approaches to refinement types (which he referred to as "contract types"). The chief problem he wanted to address is that which techniques based on using theorem provers, it's a little unpredictable whether your program will typecheck or not - you're at the whim of the TP. The idea is to figure out where you can use other techniques - e.g. fancy existentials - to get back to a more predictable system. I'd really like to consider this wrt my work on M/Oslo with Andy Gordon.

Tom Schrijvers gave a nice talk about added type invariants to Haskell. He gave a particularly nice description of the current (version 6) type system of Haskell. Whilst I like what he did, I kind of wonder whether Haskell [which I do believe to be God's own language] is going in the right direction. Or rather, whether they shouldn't just bite the bullet and become a lazy version of Coq. The power of the system that Tom presented was pretty terrifying, and as one of the questioners noted, it's now the case that programmers have to do alot (e.g. provide proofs...)

Aaron Stump gave a really nice talk about Guru - which is a language I need to check out.

In the evening we went on a long and cold walk to find a bar. After a couple of beers, Andrew, Claudio, Johannes, Barry, Christian and I had a very nice meal at 49 Bistro.

Obama

The great thing about being in the US today is that I was able to crowd around a TV with people and watch Obama become president. I have to admit to having a lump in my throat during his speech. He is a fantastic speaker:

My fellow citizens:
I stand here today humbled by the task before us, grateful for the trust you have bestowed, mindful of the sacrifices borne by our ancestors. I thank President Bush for his service to our nation, as well as the generosity and cooperation he has shown throughout this transition.
Forty-four Americans have now taken the presidential oath. The words have been spoken during rising tides of prosperity and the still waters of peace. Yet, every so often the oath is taken amidst gathering clouds and raging storms. At these moments, America has carried on not simply because of the skill or vision of those in high office, but because We the People have remained faithful to the ideals of our forbearers, and true to our founding documents.
So it has been. So it must be with this generation of Americans.
That we are in the midst of crisis is now well understood. Our nation is at war, against a far-reaching network of violence and hatred. Our economy is badly weakened, a consequence of greed and irresponsibility on the part of some, but also our collective failure to make hard choices and prepare the nation for a new age. Homes have been lost; jobs shed; businesses shuttered. Our healthcare is too costly; our schools fail too many; and each day brings further evidence that the ways we use energy strengthen our adversaries and threaten our planet.
These are the indicators of crisis, subject to data and statistics. Less measurable but no less profound is a sapping of confidence across our land - a nagging fear that America's decline is inevitable, and that the next generation must lower its sights.
Today I say to you that the challenges we face are real. They are serious and they are many. They will not be met easily or in a short span of time. But know this, America - they will be met.
On this day, we gather because we have chosen hope over fear, unity of purpose over conflict and discord.
On this day, we come to proclaim an end to the petty grievances and false promises, the recriminations and worn out dogmas, that for far too long have strangled our politics.
We remain a young nation, but in the words of Scripture, the time has come to set aside childish things. The time has come to reaffirm our enduring spirit; to choose our better history; to carry forward that precious gift, that noble idea, passed on from generation to generation: the God-given promise that all are equal, all are free, and all deserve a chance to pursue their full measure of happiness.
In reaffirming the greatness of our nation, we understand that greatness is never a given. It must be earned. Our journey has never been one of short-cuts or settling for less. It has not been the path for the faint-hearted - for those who prefer leisure over work, or seek only the pleasures of riches and fame. Rather, it has been the risk-takers, the doers, the makers of things - some celebrated but more often men and women obscure in their labour, who have carried us up the long, rugged path towards prosperity and freedom.
For us, they packed up their few worldly possessions and traveled across oceans in search of a new life.
For us, they toiled in sweatshops and settled the west; endured the lash of the whip and plowed the hard earth.
For us, they fought and died, in places like Concord and Gettysburg; Normandy and Khe Sahn.
Time and again these men and women struggled and sacrificed and worked till their hands were raw so that we might live a better life. They saw America as bigger than the sum of our individual ambitions; greater than all the differences of birth or wealth or faction.
This is the journey we continue today. We remain the most prosperous, powerful nation on Earth. Our workers are no less productive than when this crisis began. Our minds are no less inventive, our goods and services no less needed than they were last week or last month or last year. Our capacity remains undiminished. But our time of standing pat, of protecting narrow interests and putting off unpleasant decisions - that time has surely passed. Starting today, we must pick ourselves up, dust ourselves off, and begin again the work of remaking America.
For everywhere we look, there is work to be done. The state of the economy calls for action, bold and swift, and we will act - not only to create new jobs, but to lay a new foundation for growth. We will build the roads and bridges, the electric grids and digital lines that feed our commerce and bind us together. We will restore science to its rightful place, and wield technology's wonders to raise healthcare's quality and lower its cost.
We will harness the sun and the winds and the soil to fuel our cars and run our factories. And we will transform our schools and colleges and universities to meet the demands of a new age. All this we can do. And all this we will do.
Now, there are some who question the scale of our ambitions - who suggest that our system cannot tolerate too many big plans. Their memories are short. For they have forgotten what this country has already done; what free men and women can achieve when imagination is joined to common purpose, and necessity to courage. What the cynics fail to understand is that the ground has shifted beneath them - that the stale political arguments that have consumed us for so long no longer apply. The question we ask today is not whether our government is too big or too small, but whether it works - whether it helps families find jobs at a decent wage, care they can afford, a retirement that is dignified. Where the answer is yes, we intend to move forward. Where the answer is no, programs will end. And those of us who manage the public's dollars will be held to account - to spend wisely, reform bad habits and do our business in the light of day - because only then can we restore the vital trust between a people and their government.
Nor is the question before us whether the market is a force for good or ill. Its power to generate wealth and expand freedom is unmatched, but this crisis has reminded us that without a watchful eye, the market can spin out of control - and that a nation cannot prosper long when it favours only the prosperous. The success of our economy has always depended not just on the size of our gross domestic product, but on the reach of our prosperity; on our ability to extend opportunity to every willing heart - not out of charity, but because it is the surest route to our common good.
As for our common defence, we reject as false the choice between our safety and our ideals. Our founding fathers, faced with perils we can scarcely imagine, drafted a charter to assure the rule of law and the rights of man, a charter expanded by the blood of generations. Those ideals still light the world, and we will not give them up for expedience's sake. And so to all other peoples and governments who are watching today, from the grandest capitals to the small village where my father was born: know that America is a friend of each nation and every man, woman and child who seeks a future of peace and dignity, and that we are ready to lead once more.
Recall that earlier generations faced down fascism and communism not just with missiles and tanks, but with sturdy alliances and enduring convictions. They understood that our power alone cannot protect us, nor does it entitle us to do as we please. Instead, they knew that our power grows through its prudent use; our security emanates from the justness of our cause, the force of our example, the tempering qualities of humility and restraint.
We are the keepers of this legacy. Guided by these principles once more, we can meet those new threats that demand even greater effort - even greater cooperation and understanding between nations. We will begin to responsibly leave Iraq to its people, and forge a hard-earned peace in Afghanistan. With old friends and former foes, we will work tirelessly to lessen the nuclear threat, and roll back the specter of a warming planet. We will not apologise for our way of life, nor will we waver in its defence, and for those who seek to advance their aims by inducing terror and slaughtering innocents, we say to you now that our spirit is stronger and cannot be broken; you cannot outlast us, and we will defeat
you.
For we know that our patchwork heritage is a strength, not a weakness.
We are a nation of Christians and Muslims, Jews and Hindus - and non-believers. We are shaped by every language and culture, drawn from every end of this Earth; and because we have tasted the bitter swill of civil war and segregation, and emerged from that dark chapter stronger and more united, we cannot help but believe that the old hatreds shall someday pass; that the lines of tribe shall soon dissolve; that as the world grows smaller, our common humanity shall reveal itself; and that America must play its role in ushering in a new era of peace.
To the Muslim world, we seek a new way forward, based on mutual interest and mutual respect. To those leaders around the globe who seek to sow conflict, or blame their society's ills on the west - know that your people will judge you on what you can build, not what you destroy. To those who cling to power through corruption and deceit and the silencing of dissent, know that you are on the wrong side of history; but that we will extend a hand if you are willing to unclench your fist.
To the people of poor nations, we pledge to work alongside you to make your farms flourish and let clean waters flow; to nourish starved bodies and feed hungry minds. And to those nations like ours that enjoy relative plenty, we say we can no longer afford indifference to suffering outside our borders; nor can we consume the world's resources without regard to effect. For the world has changed, and we must change with it.
As we consider the road that unfolds before us, we remember with humble gratitude those brave Americans who, at this very hour, patrol far-off deserts and distant mountains.
They have something to tell us today, just as the fallen heroes who lie in Arlington whisper through the ages. We honour them not only because they are guardians of our liberty, but because they embody the spirit of service; a willingness to find meaning in something greater than themselves. And yet, at this moment - a moment that will define a generation - it is precisely this spirit that must inhabit us all.
For as much as government can do and must do, it is ultimately the faith and determination of the American people upon which this nation relies. It is the kindness to take in a stranger when the levees break, the selflessness of workers who would rather cut their hours than see a friend lose their job which sees us through our darkest hours. It is the firefighter's courage to storm a stairway filled with smoke, but also a parent's willingness to nurture a child, that finally decides our fate.
Our challenges may be new. The instruments with which we meet them may be new. But those values upon which our success depends - hard work and honesty, courage and fair play, tolerance and curiosity, loyalty and patriotism - these things are old. These things are true. They have been the quiet force of progress
throughout our history. What is demanded then is a return to these truths. What is required of us now is a new era of responsibility - a recognition, on the part of every American, that we have duties to ourselves, our nation, and the world, duties that we do not grudgingly accept but rather seize gladly, firm in the knowledge that there is nothing so satisfying to the spirit, so defining of our character, than giving our all to a difficult task.
This is the price and the promise of citizenship.
This is the source of our confidence - the knowledge that God calls on us to shape an uncertain destiny.
This is the meaning of our liberty and our creed - why men and women and children of every race and every faith can join in celebration across this magnificent mall, and why a man whose father less than sixty years ago might not have been served at a local restaurant can now stand before you to take a most sacred oath.
So let us mark this day with remembrance, of who we are and how far we have traveled.
In the year of America's birth, in the coldest of months, a small band of patriots huddled by dying campfires on the shores of an icy river. The capital was abandoned. The enemy was advancing. The snow was stained with blood. At a moment when the outcome of our revolution was most in doubt, the father of our nation ordered these words be read to the people:
"Let it be told to the future world...that in the depth of winter, when nothing but hope and virtue could survive...that the city and the country, alarmed at one common danger, came forth to meet [it]."
America. In the face of our common dangers, in this winter of our hardship, let us remember these timeless words. With hope and virtue, let us brave once more the icy currents, and endure what storms may come. Let it be said by our children's children that when we were tested we refused to let this journey end, that we did not turn back nor did we falter; and with eyes fixed on the horizon and God's grace upon us, we carried forth that great gift of freedom and delivered it safely to future generations.

I'm in Savannah

I'm in Savannah attending POPL and some associated events (PLPV and PLAN-X). I'll try to blog about the talks later.

I arrived last night. We flew from London to Washington DC. No-one realized when we booked the flight that we'd be trying to get a connecting flight the day before Barack Obama's inaugration! The flight over was okay (but I don't think that Virgin is any better than BA - in fact, BA has a better entertainment system...). The one amusing thing was that my neighbour - from Sudan - was using a pen advertising the "Arrive Alive Driving School" in Lagos. Wow! Now that's what I call direct advertising :-)

When we arrived in DC there was a huge queue for passport control. Luckily I sweet-talked the woman into letting us get to the front (after waiting for around an hour!). After a sprint to the United desk, I discovered the connection was delayed, so panic over.

The hotel is nice, and I have a great room overlooking the river.

Sony Vaio P

Look here.

If the question is "Sexier than the Eee girl?", then the answer is surely yes!

Congratulations James!

Congratulations to my hugely talented brother James who has just been appointed as the Executive Producer at the Donmar Warehouse. (See also here and here.) To quote Micheal Grandage:

James has been the most wonderful collaborator and a great spokesman for the Donmar since he joined us. He is, without doubt, one of the most exciting new producers to emerge in recent years. His expertise, energy and enthusiasm are a wonderful addition to the Donmar’s core Executive, and I’m thrilled he has been offered the post as we look ahead to the next few years of our development.

I'm very proud. (As one of my colleagues put it: "So he's the successful one then".)

Functional Programming - Tipping point

Has functional programming finally reached the tipping point? I don't know but here's a good sign: it is on the front cover of Dr Dobbs this month. [Slightly strange that the first language they mention is Scala. However they do discuss my current preferred language, F#; and God's own language: Haskell.]

MSR Products

Microsoft Research has recently started selling some of its research software as real products. One of the first was AutoCollage that was developed by guys here in MSR Cambridge. This is a very nice tool - I have a collage of the girls on my office wall generated by the beta version.

The latest product is SongSmith. This is a very cute app that automatically generates musical accompaniment to a vocal line (supplied by you!). The demo video is very neat. The girls would love this!

Both are available at credit-crunch-prices (TM): $19 for AutoCollage and $29 for SongSmith (although the website wouldn't let me buy SongSmith five minutes ago - probably still being updated...).

Zune bug

Turns out that the problem that froze everyone's Zune 30 is down to a schoolboy programming bug :-(

My colleague, Byron Cook's terminator tool would have found this bug. Shame more people aren't using it!

Dinner party

Last night we went to a lovely dinner party at Lucy (winner of the Ian Charleson Award in 1996) and David's. The highlights were:

• The food! Starter: Spicy prawns and spring rolls. Main: Meat and Vegetarian chilli with salad and garlic bread. Desert: Pavlova and Chocolate and Chestnut Torte. Yum!
• Judith's confession that she got in trouble with her headmaster for mis-behaving on Songs of Praise.
• The Kennedys are on youtube!
• The amazing details associated with sexual hygiene products.
• The best business card job title: "R&D, toilet products - solids and liquids".

A great evening.

Worst film ever

Whilst in Slovenia, we tend to watch whatever film is on that's in English. It's a bit of a lottery: this trip I enjoyed Matchstick Men. However, I think I did watch the Worst Film Ever (TM): Meet the Santas. Unspeakably awful...