Friday, 19 December 2008
Tuesday, 16 December 2008
Monday, 15 December 2008
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!]
Saturday, 6 December 2008
Wednesday, 3 December 2008
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.
Thursday, 27 November 2008
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!
Wednesday, 19 November 2008
Thursday, 13 November 2008
[There's stuff on the web if you want to take a look. Here's some material on ZDNet. ]
Tuesday, 11 November 2008
Friday, 7 November 2008
[If you don't have it already, the latest Radiohead album "In Rainbows" is, in my opinion, a work of genuis.]
Tuesday, 4 November 2008
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!
Friday, 31 October 2008
Wednesday, 29 October 2008
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 :-)
Tuesday, 28 October 2008
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 :-( ]
Wednesday, 22 October 2008
Monday, 20 October 2008
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!
Thursday, 9 October 2008
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.
Thursday, 2 October 2008
Wednesday, 1 October 2008
Thursday, 25 September 2008
Monday, 22 September 2008
Friday, 19 September 2008
Wednesday, 10 September 2008
Friday, 5 September 2008
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.
Tuesday, 2 September 2008
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...]
Thursday, 28 August 2008
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.
Tuesday, 19 August 2008
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!]
Saturday, 16 August 2008
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!
Thursday, 14 August 2008
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...
Wednesday, 30 July 2008
What's next? Guerilla category theory?
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
Wednesday, 16 July 2008
Friday, 11 July 2008
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!
Thursday, 10 July 2008
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!
Wednesday, 9 July 2008
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...
Tuesday, 8 July 2008
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.
Tuesday, 1 July 2008
Monday, 30 June 2008
Thursday, 26 June 2008
Monday, 23 June 2008
Wednesday, 18 June 2008
Monday, 16 June 2008
[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.
Friday, 6 June 2008
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!
Thursday, 29 May 2008
Looking at the ZDNet website, it seems that Ed has also included a number of other posts to help people "improve" their Vista experience.
Wednesday, 28 May 2008
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...
Thursday, 22 May 2008
Tuesday, 13 May 2008
It's been a long time in coming - but enjoy! There are some great papers.
Thursday, 8 May 2008
Wednesday, 7 May 2008
Tuesday, 6 May 2008
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!
- Matthew and Dino's paper on JStar, which is their separation logic based tool for verifying Java programs.
- Claudio's paper on his implementation of joins in the production Visual Basic Compiler.
Well done guys!
Wednesday, 30 April 2008
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).
Tuesday, 29 April 2008
Thursday, 24 April 2008
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!
Monday, 14 April 2008
Wednesday, 9 April 2008
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...
Wednesday, 19 March 2008
Tuesday, 18 March 2008
Monday, 17 March 2008
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 :-)
Sunday, 9 March 2008
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 :-)
Friday, 7 March 2008
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 :-)
Thursday, 6 March 2008
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!)
Wednesday, 5 March 2008
...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.
Friday, 29 February 2008
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
Wednesday, 27 February 2008
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...)
Monday, 25 February 2008
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).
Tuesday, 19 February 2008
Wednesday, 13 February 2008
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.
Monday, 4 February 2008
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.