Wednesday, 30 January 2008
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
Tuesday, 22 January 2008
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
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 :-)
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
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 :-(
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:
- They tried C# before moving to OCAML. They dropped C# because of code verbosity and the difficulty of reasoning about their code.
- 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
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.
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
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.