Wednesday 30 January 2008

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.

Thursday 24 January 2008

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:




Tuesday 22 January 2008

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.

Monday 21 January 2008

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.

Tuesday 15 January 2008

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 :-)

Saturday 12 January 2008

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.

Thursday 10 January 2008

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.

Tuesday 8 January 2008

POPL'08

Tomorrow I head off to San Francisco to attend POPL 2008. Matthew will be presenting some joint work on verifying OO programs.

I will try to blog during the conference. The program looks very exciting so I'm looking forward to attending!

Friday 4 January 2008

An answer to a question

Just in case there's someone who hasn't seen this clip before: click here.