Posted by
The Symposium on Principles of Programming Languages (opens in new tab) (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 (opens in new tab).
Ideas: Exploring AI frontiers with Rafah Hosn
Energized by disruption, partner group product manager Rafah Hosn is helping to drive scientific advancement in AI for Microsoft. She talks about the mindset needed to work at the frontiers of AI and how the research-to-product pipeline is changing in the GenAI era.
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 (opens in new tab) team from Microsoft Research Redmond (opens in new tab), the Programming Principles and Tools (opens in new tab) group from Microsoft Research Cambridge (opens in new tab), and the Programming Languages and Tools (opens in new tab) unit from Microsoft Research India (opens in new tab).
It’s only natural, says Judith Bishop (opens in new tab), director of Computer Science (opens in new tab) for Microsoft Research Connections (opens in new tab).
“Microsoft has a long tradition of innovation in programming languages,” she says, “with C# and F# (opens in new tab) being two that have become part of the Windows (opens in new tab) 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 (opens in new tab) of Try F# (opens in new tab), 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 (opens in new tab), one of the events co-located with POPL, will be held Jan. 22, with Evelyne Viegas (opens in new tab) 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 (opens in new tab), 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 (opens in new tab) of Microsoft Research Cambridge; Sebastian Burckhardt (opens in new tab), Manuel Fahndrich (opens in new tab), and Francesco Logozzo (opens in new tab) of Microsoft Research Redmond; and Sriram Rajamani (opens in new tab) of Microsoft Research India.
- The 2012 Microsoft Research Verified Software Milestone Award (opens in new tab) will be presented to Xavier Leroy (opens in new tab) of the Paris-Rocquencourt (opens in new tab) research center of Inria (opens in new tab).
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 (opens in new tab) of Microsoft Research Cambridge; Nikhil Swamy (opens in new tab), Juan Chen (opens in new tab), and Benjamin Livshits (opens in new tab) 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 (opens in new tab).
Another of the Microsoft Research co-authored papers is Synthesis of Biological Models from Mutation Experiments, by Ali Sinan Köksal, Yewen Pu, Saurabh Srivastava, and Rastislav Bodik of the University of California, Berkeley; Nir Piterman of the University of Leicester; and Jasmin Fisher (opens in new tab) 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 (opens in new tab), 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 (opens in new tab), as well as for his leadership of that development team. The CompCert (opens in new tab) 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.”