Wandering through the streets of Madrid, alive with people socializing until late at night, I was reminded of the importance of networking and collaboration. For Microsoft Research, it is our lifeblood. Through our joint research centers (opens in new tab), along with internships, scholarships, fellowships, and visitor programs (opens in new tab), we remain connected to researchers who share our passion to use computing to improve lives. Last month, those connections were on full display as we celebrated our collaborations with European institutions during the Microsoft Research IMDEA Software Institute Collaboration Workshop (MICW (opens in new tab)).
The Microsoft IMDEA Software Joint Research Centre (opens in new tab) was formed in 2014. This collaborative venture between Microsoft Research and the IMDEA Software Institute (opens in new tab) fosters work on topics of mutual interest in the following broad categories: scalable and correct data management in the cloud, verification for cryptography and security, and secure distributed programming. A distinctive event organized by the center is the annual MICW, now in its second year. I was keen to see what progress had been made and what projects would emerge to offer real, positive results. I was not disappointed, nor, I suspect, were the other 50 attendees.
The workshop brought together researchers and students to discuss their collaborative work on hot topics in software.
Spotlight: Microsoft research newsletter
Microsoft Research Newsletter
At the top of the list is F* (opens in new tab), a project that involves our Redmond and Cambridge Labs as well as IMDEA and Inria (opens in new tab) in France. F* is a new higher order programming language (like ML), designed with program verification in mind. F* allows for the expression of precise and compact specifications for programs, including functional correctness properties. The F* type-checker works behind the scenes to prove that programs meet their specifications by using an automated theorem prover (usually Z3 (opens in new tab)) to discharge proof obligations. Programs written in F* can be translated to OCaml, F#, or JavaScript for execution.
F* has already been used to verify implementations of cryptographic constructions and protocols (opens in new tab) and web browser extensions (opens in new tab), to verify the formalization of the semantics of other languages (including JavaScript and a compiler from a subset of F* to JavaScript (opens in new tab) and TS*, a secure subset of TypeScript (opens in new tab)), and even to certify the correctness of the core of F* type-checker itself (opens in new tab).
The latest version of F* is written entirely in F*, and bootstraps in OCaml and F#. It is open source and under active development on GitHub (opens in new tab). Many people are surprised to learn that Microsoft has so much open-source software, but even .NET is now open-sourced through the .NET Foundation (opens in new tab).
Another exciting project, Orleans (opens in new tab), was the topic of an inspiring keynote by Microsoft Distinguished Scientist Phil Bernstein. As Phil explained, Orleans is a framework that provides a straightforward approach to building distributed high-scale computing applications, without the need to learn and apply complex concurrency or other scaling patterns.
Created by Microsoft Research and designed for use in the cloud, Orleans has been deployed extensively by several Microsoft product groups, most notably by 343 Industries, which is using it as a platform for all Halo 4 cloud services. Many of the attendees were impressed that a system powering the world’s most popular game is open source, a fact that further underscores Microsoft’s deep commitment to open development, which we believe fosters community participation and collaboration, encourages innovation, and broadens and strengthens the future of IT.
Phil Bernstein spoke about Orleans, a straightforward approach to building distributed high-scale computing applications.
This commitment to collaboration was also evident during the extensive discussion periods, as when Kapil Vaswani from Microsoft Research India asked whether attendees could develop criteria for checking the robustness of cloud applications (in particular, under weakening transactions to causality), by applying the criteria to case studies from Orleans and other domains. The work would build on static analysis algorithms, which are a particular strength of Microsoft researchers, and would profit from the unique expertise brought by outside researchers.
—Judith Bishop (opens in new tab), Director of Computer Science, Microsoft Research, and Cédric Fournet (opens in new tab), Principal Researcher, Microsoft Research
Learn more