Arrivederci, Roma: As the 40th ACM Principles of Programming Languages conference (POPL 2013) drew to a close on Friday, January 25, 2013, I was struck by how much it was a celebration of excellence, and I was pleased that Microsoft Research could play a big part in that. With three of our labs represented—Cambridge, India, and Redmond—Microsoft Research attendees presented 10 of the 43 papers in the main conference and 11 more throughout the week, hosted a new workshop, and lent a substantial hand in the conference’s organization.
Just getting in to POPL—with its 18 percent acceptance rate—signifies excellence, but as the following highlights demonstrate, the level of achievement among this year’s attendees was off the charts.
Judith Bishop (left) of Microsoft Research Connections and Natarajan Shankar (right) from SRI, on the Verified Software Initiative, present Xavier Leroy (center) from INRIA with the Verified Software Milestone Award 2012.
Georges Gonthier from Microsoft Research Cambridge presented the opening keynote address. In a rousing manner, he described how he and a team at INRIA (France’s national institute for computational sciences) spent six years chasing a proof in group theory, and how they finally managed to solve it by using Coq, a language and tool that is available across various platforms, soon to include Windows 8. Group theory has been used to explain how atomic particles combine and serves as a base for cryptography, itself an important part of security, a theme that recurred throughout the conference. I spotted Georges chatting with students at the Microsoft table during the breaks, carefully explaining his work and encouraging his listeners to go further. I felt proud to have him as a colleague.
INRIA was mentioned again when I presented the second Microsoft Research Verified Software Milestone Award to Xavier Leroy, architect of the CompCert C verified compiler and the leader of the INRIA team that implemented it. This award, initiated by Microsoft Research’s Tony Hoare and offered by the Verified Software Initiative, honors true milestones in verifying software. Xavier was a very popular choice, and I reflected on how important it is to engage in such research as we face increasing cyber attacks on every program we write.
From celebrating the present we went to looking at the past. POPL began in 1973, and Dartmouth’s Doug McIlroy, who had been at that first conference, gave a humorous account of the topics that were covered and how they differed—and yet did not differ—from what we discuss today. Then there was a true moment of excellence: the most famous Italian computer scientist, Corrado Böhm, was recognized with the presentation of a scroll by Roberto Giacobazzi, general chair of POPL. In 1953, before FORTRAN and ALGOL were even specified, Corrado wrote a thesis on compiling a language in itself, using lambda calculus. He went on to train generations of computer scientists in Italy. With his wife and family by his side, he received a standing ovation from the POPL community.
Back at the Microsoft Research table, the 22 researchers at POPL had many interesting chats with students and faculty, focusing on how we face the challenge of making our research and teaching—in the words of Corrado Böhm—“simple, general, and abstract.” Better languages, with better security and wider applicability, help us achieve those goals. I’m certain that the next POPL will find us another step further along in the pursuit of excellence.
—Judith Bishop, Director of Computer Science, Microsoft Research Connections