A Toosht o Whigmaleeries

Do consider submitting to PADL, co-located with POPL, in Savannah, Georgia, next January.

Submission deadline: September 9

http://cs.utdallas.edu/padl09/

At the UKCRC AGM yesterday, Mark Josephs pointed me at a demo of WSE 3.0 and our Policy Advisor by my buddy Jason Hogg.

The Web Services Enhancements (WSE) are a series of Microsoft products that implement web services standards such as WS-Security and WS-SecureConversation.  We used the WSE implementations as the basis of our empirical work in the Samoa Project (roughly 2003 till 2007).  We built some formal verification tools, such as TulaFale and FS2PV, for describing and verifying security properties of web services (and other) security protocols.  In the process, we found lots of ways to misconfigure WSE, and so we also built some Policy Advisors, which provide no formal guarantees, but identify a range of potential misconfigurations.  In the webcast, Jason demos the version of Policy Advisor that ships with WSE 3.0.

We just completed a paper that's to appear at ESORICS 2008:

Code-Carrying Authorization

S. Maffeis, M. Abadi, C. Fournet, and A.D. Gordon

In authorization, there is often a wish to shift the burden of proof to those making requests, since they may have more resources and more specific knowledge to construct the required proofs. We introduce an extreme instance of this approach, which we call Code-Carrying Authorization (CCA). With CCA, access-control decisions can partly be delegated to untrusted code obtained at run-time. The dynamic verification of this code ensures the safety of authorization decisions. We define and study this approach in the setting of a higher-order spi calculus. The type system of this calculus provides the needed support for static and dynamic verification.

Super interesting paper:

Towards a Model of Computer Systems Research

Thomas Anderson

This paper develops a model of computer systems research as a way of helping explain to prospective authors the often obscure workings of conference program committees. While our goal is primarily descriptive, we use the model to motivate several recent changes in conference design and to suggest some further potential improvements.

Andy Hopper of the Computer Lab, is to lecture on "Computing for the Future of the Planet" at the UK Computing Research Committee annual assembly on Monday 14 July.  I'm looking forward to it!

Digital technology is becoming an indispensable and crucial component of our lives, society, and environment. A framework for computing in the context of problems facing the planet will be presented. The framework has a number of goals: an optimal digital infrastructure, sensing and optimising with a global world model, reliably predicting and reacting to our environment, and digital alternatives to physical activities.

Cyd Charisse is just great in Singin' in the Rain, a movie that always cheers me up.  May she rest in peace.

I usually enjoy the obituaries in the King's College Annual Report, and the 2007 annual report is no exception.

"Roger (Roger John King, who came up to Cambridge in 1962) looked back on his time at King's with mixed feelings.  He had a keen sense of himself as a 'grammar school boy' and this was something he wryly liked to stress.  It was always claimed that while at King's he never properly unpacked his suitcases from home, perhaps as a statement that he felt he did not entirely belong in Cambridge but had been stranded there by mistake.  He never had the money to eat out and took all his meals in Hall, and possibly as a result of this developed a mild case of scurvy, after which fruit began to appear on the menu."

Can you believe it?  Scurvy, in England, in 1962?  Began to appear, so that would be weekly, perhaps?

Notwithstanding his youthful deficiency in Vitamin C, Mr King appears to have had a grand old life, interviewing a youthful George Harrison at the time of the Beatles one and only concert in Cambridge, writing a PhD dissertation on crime fiction (it was the 60s after all), and being a successful academic.  Good on him, and may he rest in peace.

Following up my previous post, Mitch Wand writes describing an outcome of the Harvard meeting, a move to include FP in the ACM standard curriculum.  Message below.  Thanks, Mitch!

The ACM Curriculum board has re-opened the 2001 design for review.  Although ACM is a US-based organization, the curriculum is not only influential at the middle tier of US colleges and universities, it is also taken seriously by many evolving and developing educational institutions overseas. In recent years, the study of non-OO PLs, and of other key PL topics such as type systems, has grown increasingly marginal in the undergraduate CS curriculum. In particular, the study of functional programming is not included the ACM CS2001 core. We may now have an opening to make a small change in this situation.
The ACM Curriculum board has agreed to consider a proposal on including FP as an equal to OOP (10 "hours" each) in the standard curriculum. This was the most concrete outcome of the PLC workshop at Harvard two weeks ago. The proposal was drafted by Stuart Reges, Shriram Krishnamurthi, and Matthias Felleisen and was endorsed unanimously by the workshop attendees and by the SIGPLAN Executive Committee. It proceeds on the premise that inclusion of FP in the core curriculum is the most important single thing that the PL community can do for CS education. In particular, this will help prepare students for a properly designed though possibly optional PL course or courses.
Please consider contributing comments to the web site. A simple "Yes, I think this is a great idea" will be helpful. A short explanation is even better.
There is now a long list of comments supporting this proposal. However, we have very few comments from people in industry, so comments from non-academics would be particularly helpful. (Please identify yourself as a practitioner, too.) 
The web site is http://wiki.acm.org/cs2001/index.php?title=SIGPLAN_Proposal.

Interesting piece from some mathematical societies on the use of citation stats to assess research quality.  The theme is that: "Numbers are not inherently superior to sound judgements."

I'd a good time at a workshop yesterday and today at Imperial College for "Young Researchers on Service-Oriented Computing" (YRSOC).  It was rather flattering to be invited to give a talk as I am not especially young, but hey.  It was a good crowd and I enjoyed the talks and conversations.

Thanks especially to Monika Solanki for the invitation.  She and Barry Norton did a great job of running the show.  During a great conversation, she told me about a meeting this week on "Washington, Wikipedia, and Web 3.0"?  3.0 already?

Funnily enough, my last visit to Imperial was for WS-BPI, in February, a workshop on a rather similar topic (modulo age) - business processes and web services - but there was not much overlap between the attendees.  Lots of session types at WS-BPI, and lots of BPEL at YRSOC.

There was a workshop recently at Harvard on undergraduate programming language curricula.  A great many of my university colleagues were there.  Going on the contributed papers, it looks like the meeting was a lot of fun, and is a testament to the central place in computer science of programming languages.

As I type, Karthik is presenting our Baltic paper "Service Combinators for Farming Virtual Machines" at Coordination in Oslo.

We tried to fly out on Tuesday but there was a bomb scare at City airport - a real, live, WWII bomb discovered during excavations for the Olympics.  Bah, I gave up, shame on me (though I blame the Luftwaffe), but Karthik persisted and went out yesterday.

Hope the talk's going well, man!

Andrej Bauer took my picture after my talk at MFPS in Philadelphia last week.  He was threatening to place it on his Photos of Mathematicians page.  Funnily enough, I see myself as a computer scientist and not a mathematician, but anyway I will take this as a compliment.  In any case, the picture isn't there yet, but maybe soon?

Speaking of MFPS, Benjamin Pierce shocked everyone with his new position, Types Considered Harmful.

The LASER summer school this September looks like great fun!  I hope they put their slides on the web.

We had a lot of fun at R2D2 last week.

Our website http://research.microsoft.com/riseandrise hosts various records of the meeting:

· PDFs of all the talks at the meeting (the talks by Paul Anderson and John Wilkes are good places to start)

· The proceedings consisting of 16 position papers

Two days to R2D2; we're suggesting that participants wanting to meet on the Sunday night gather at the Castle Inn, from 9pm.

See you there!

Today we posted the preliminary schedule for the MSR/HP Labs research meeting on the Rise and Rise of the Declarative Datacentre, which takes place in a couple of weeks on May 12 and May 13.  We have drawn together quite a diverse range of folks interested in applying declarative techniques for programming and managing computations in datacentres.  By bringing together folks who would not ordinarily meet we hope to sow the seeds for some serendipities.  Should be fun!

Note to self: check this out some time.  Though frankly it's in a different direction than my favourite cartoonist, Jessica Abel.  We love ArtBabe.

Materials from this seminar, from October 2007, are now available online.  There is a picture of the participants; that's me on the left!

Good to hear: USENIX announces "All online conference proceedings are now freely available to everyone. This significant decision will allow universal access to some of the most important technical research in advanced computing. In making this move USENIX is setting the standard for open access to information, an essential part of its mission. Click here for more information."

The next MSR call for PhD scholarships is out; the deadline is 10 September 2008.

As previous years, applications must be made by PhD supervisors not by students. Supervisors will be informed of our decision in November 2008 and will then have up to a year to find the best student possible for the proposed project. Students will typically start their PhD in October 2009.

I already mentioned WS-BPI, which took place at Imperial on February 7 and 8.  The slide decks are now available.  After some years, there are signs here of fruitful interactions between the semantics community and industrialists interested in web services.

I had a short but sweet visit to Thomas Wilke's group at the University of Kiel.  Kiel is of course on the Baltic, so the view below from their building shows the blue waters of the Baltic Sea in the distance.

As you may expect, I gave my Baltic talk, by the Baltic.  I also had some stimulating discussions about Thomas' group work on web services security, logics of knowledge, and contract signing protocols.

Mike Gordon has been spreading the good news that Robin Milner has been honoured in the USA.  From the press release:

Arthur John Robin Gorell Milner, emeritus professor, University of Cambridge, Cambridge, U.K. For fundamental contributions to computer science, including the development of LCF, ML, CCS, and the pi-calculus.

After the first and the second last year, this year sees the third and final special issue of JLAP devoted to papers from the 2005 Bertinoro meeting on algebraic process calculi.

Volume 75, Issue 1, Pages 1-166 (February-March 2008)

Algebraic Process Calculi. The First Twenty Five Years and Beyond. III
Edited by L. Aceto, M. Bravetti, W. Fokkink and A.D. Gordon

Automated verification of selected equivalences for security protocols
Bruno Blanchet, Martín Abadi and Cédric Fournet

A process algebraic view of shared dataspace coordination
Nadia Busi and Gianluigi Zavattaro

Behavioural equivalences for dynamic Web data
Sergio Maffeis and Philippa Gardner

CCS with priority guards
Iain Phillips

As Luca reports, our community was shocked and saddened by the news that Nadia Busi died in September.  May she rest in peace.