Microsoft Research Blog

The Microsoft Research blog provides in-depth views and perspectives from our researchers, scientists and engineers, plus announcements about noteworthy events, scholarships, and fellowships designed for academic and scientific communities.

Programming Languages in the Eternal City

January 22, 2013 | Posted by Microsoft Research Blog

Posted by Rob Knies

POPL 2014 logo

The Symposium on Principles of Programming Languages (POPL) is an annual gathering of thought leaders from around the world to discuss all aspects of programming languages and systems, so it is a given that as the 40th instance of the event gets under way in Rome on Jan. 23, Microsoft Research will be providing robust support.

Twenty-two papers, co-written by a total of 36 Microsoft Research scientists, were selected for presentation during the symposium, which concludes Jan. 25, and its co-located events—which began Jan. 20 and run through Jan. 26. Twenty attendees, spanning the Research in Software Engineering team from Microsoft Research Redmond, the Programming Principles and Tools group from Microsoft Research Cambridge, and the Programming Languages and Tools unit from Microsoft Research India.

It’s only natural, says Judith Bishop, director of Computer Science for Microsoft Research Connections.

“Microsoft has a long tradition of innovation in programming languages,” she says, “with C# and F# being two that have become part of the Windows ecosystem in the past decade. Microsoft Research also looks ahead at the wider issues discussed during POPL on how principles underpin practice.

“Security of code, speedup through concurrency, and abstraction for easier creation of code are all aspects covered by our researchers. With researchers in programming-languages groups in three Microsoft Research labs across the globe, POPL serves as a forum where we can meet other experts and inspire the upcoming talents of new graduates.”

In addition to serving as a sponsor of the event, Microsoft Research will be involved in a broad array of POPL activities, including:

  • The gold release of Try F#, a collection of tools that make it easy to learn the F# language, create programs, explore rich data sets, and write and share code with the community from a familiar, browser-based experience.
  • The Data Driven Functional Programming Workshop, one of the events co-located with POPL, will be held Jan. 22, with Evelyne Viegas of Microsoft Research Connections serving as general chair and Bishop acting as program co-chair. The workshop will examine data-centric programming in today’s era of big data, focusing on the application of functional programming and meta-programming techniques.
  • Georges Gonthier, principal researcher at Microsoft Research Cambridge, will deliver a Jan. 23 keynote entitled Engineering Mathematics: The Odd Order Theorem Proof, which will address his recent proof of the Feit-Thompson Theorem.
  • Technologies and academic programs from Microsoft Research Connections for the greater research community.
  • Five scientists from Microsoft Research are serving on the POPL program committee, including Josh Berdine of Microsoft Research Cambridge; Sebastian Burckhardt, Manuel Fahndrich, and Francesco Logozzo of Microsoft Research Redmond; and Sriram Rajamani of Microsoft Research India.
  • The 2012 Microsoft Research Verified Software Milestone Award will be presented to Xavier Leroy of the Paris-Rocquencourt research center of Inria.

The submitted papers from Microsoft Research cover a wide range of topics related to programming languages, and Bishop provides a preview.

“Two of the exciting results involve security and biology,” she relates. “Our researchers in Cambridge and Redmond worked with Inria to develop a compiler that guarantees the correctness for whole programs executing within arbitrary JavaScript browser contexts. They evaluated the compiler on sample programs, including a series of secure libraries.”

That paper—written by Cédric Fournet of Microsoft Research Cambridge; Nikhil Swamy, Juan Chen, and Benjamin Livshits of Microsoft Research Redmond; Pierre-Evariste Dagand of Scotland’s University of Strathclyde; and Pierre-Yves Strub of the Madrid Institute for Advanced Studies in Software Development Technologies—is entitled Jasmin Fisher of Microsoft Research Cambridge.

“Diseases can be caused by perturbed gene and protein regulatory networks,” Bishop explains. “Experimental biologists are concerned about the correctness of their models. Unfortunately, turning informal maps of regulatory networks common in biological literature into executable models is laborious, because it involves explicitly defining timing delay and strength of how multiple proteins regulate each other.

“This paper develops techniques for synthesizing executable models from experimental observations and prior biological knowledge.”

The Try F# release, Viegas says, is a way to encourage those who work with programming-languages to sample the capabilities offered by F#.

“We want to entice the programming-language community to look in particular at the information-rich programming paradigm of F# 3.0,” she says, “and how we’ve made it easy to bring data and metadata from big, broad data to the fingertips of the programmer. Try F# includes great tutorials to help programmers and data scientists learn about this new paradigm, try it out with code creation in record time, and be able to share the experience and code with the community.”

Gonthier, meanwhile, will share insights on his proof of the Feit-Thompson Theorem, achieved in part with the Coq proof assistant, developed at the Microsoft Research-Inria Joint Centre, based in Palaiseau, outside of Paris.

The theorem, also known as the Odd-Order Theorem, states that in mathematical group theory, every finite group of odd order is solvable. The proof has significant applicability to computer science, because group theory is the base for most cryptography schemes.

During a plenary session, the Microsoft Research Verified Software Milestone Award was presented to Leroy to recognize his role as architect of the CompCert C Verified Compiler, as well as for his leadership of that development team. The CompCert project investigates the formal verification of realistic compilers usable for critical embedded software, and Leroy’s contribution is a high-assurance compiler for almost all of the ISO C90/ANSI C language, generating efficient code for PowerPC, ARM, and x86 processors.

“Microsoft Research is delighted to celebrate the advances made by Dr. Leroy in the vital field of software verification,” Bishop says. “Compilers are the basis for all the software we generate, and by ruling out compiler-introduced bugs, the CompCert project has taken a huge leap in strengthening guarantees for reliable, critical embedded software across platforms.

“We congratulate Dr. Leroy on his significant achievement in winning this award.”