Microsoft Research @ POPL 2018

Microsoft Research India is actively working in the areas of program synthesis (e.g., for database query optimization) (contact: Kaushik Rajan and Akash Lal), automated testing and bug-finding for concurrent programs (contact: Akash Lal), programming secure enclaves (contact: Aseem Rastogi and Akash Lal), and parallel programming models and runtime systems (contact: Harsha Vardhan Simhadri). Students interested in any of these areas are encouraged to apply for an internship! Please indicate the appropriate contact from above in your application.

The Research in Software Engineering (RiSE) group at Microsoft Research Redmond is actively looking for strong intern candidates including those with interest in the following areas:

• Language design and semantics, program verification applied to secure networking protocols and cryptography, targeting performant code in assembly, C and WASM (contact: Nikhil Swamy)
• HPC, GPU programming, distributed systems for a large-scale machine learning project. We are also looking for people with strong linear algebra skills and theoretical machine learning expertise. (contact: Madan Musuvathi)
• Kernel programming, dynamic analysis, concurrency bug finding (contact: Madan Musuvathi)
• Neural program synthesis, AI for software engineering, and intersection of neural and symbolic AI techniques (contact: Rishabh Singh)
• Programming, debugging, and reasoning about spreadsheets (contact: Ben Zorn)
• Algebraic effects, including semantics, implementation, compilation, theoretical properties, and real-world applications (contact: Daan Leijen)

Students interested in any of these areas are encouraged to apply for an internship! Please indicate the appropriate contact from above in your application. Please see our careers site for more information on internships and careers at our Redmond lab.

An internship at Microsoft Research Cambridge gives you the opportunity to work on real problems alongside one of our full-time researchers as your mentor.

We are accepting applications now from students who are enrolled in current PhD or Masters programs relevant to our areas of research. Please see the below internship opportunities available in programming languages, compilers, security, and privacy. A listing of all internships available can be found here.

How to apply

To apply for one or more of the internships below (maximum of three), please create a profile on the Microsoft Research Careers tool. Please select the relevant supervisor’s name (your first choice, if you’re applying for more than one position) and add the reference number/s in the ‘more information about our relationship’ field. If you omit the reference number, your application may not be included when filtering for applications for that project.

See our Cambridge Lab internship listings and apply here.

Programming Languages

Functional programming and spreadsheets

Supervisors: Simon Peyton Jones, Andy Gordon, Claudio Russo, Neil Toronto, Advait Sarkar

Start Date: June/July 2018

Applications close January 31, 2018

Reference #: MSRC226

We hope to hire four interns during 2018 with a focus on using insights from functional programming to improve the experience of using spreadsheets. The exact internship project will be chosen to fit the expertise of successful applicants, but we are interested in a broad range of areas including:

• Improving the experience of authoring formulae in a spreadsheet
• Compiling spreadsheets for faster execution
• Using insights from type systems to catch programming errors sooner
• Generalisation and program synthesis
• Demonstrating radical improvements in the range of applications that can be tackled with spreadsheets. We are looking for three interns with programming-language expertise, and one with a strong background in HCI and user experience.

You would be working with leaders in both functional programming (Andy Gordon, Simon Peyton Jones) and user experience (Advait Sarkar, Kenton O’Hara). There is a genuine possibility that your work could have real-world impact.

By way of general background, you may want to read Simon Peyton Jones et al’s papers “A user-centred approach to functions in Excel” and “Champagne Prototyping: A Research Technique for Early Evaluation of Complex End-User Programming Systems”.

Concept C#

Supervisor: Claudio Russo

Start Date: June/July 2018 or earlier

Applications close: Feb 2, 2018

Reference #: MSRC232

Concept C# is an extension of C# with Haskell- style type classes, allowing efficient abstraction over static as well as instance members. Concept C# leverages the distinctive type-passing, code-specializing implementation of .NET Generics to provide excellent performance, competitive with hand-specialized code.

The aim of this internship would be to further the design and implementation of Concept C# to support better concept inference with a well-defined logic, associated types, and constraint propagation. The last two features would greatly reduce the notational burden for advanced uses and go a long way to addressing the remaining concerns of the C# language design team (who are very supportive of this work). There is a publication describing the basic mechanism for a slightly different system so the task would be to adapt, design and implement that proposal in our working prototype of Concept C# already implemented over two internships by intern Matt Windsor. The concept code is extremely well documented and should be straightforward for another good intern to build on. The intern would gain experience of practical language design and engineering on a large, yet approachable, compiler code base (Roslyn) with the potential for real tech transfer.

Contact: crusso@microsoft.com

Accelerating machine learning on specialized hardware

Supervisors: Dimitrios Vytiniotis, Ryota Tomioka

Start Date: Spring or Summer 2018

Applications close: March 1, 2018

Reference #: MSRC233

The focus of this internship will be on compilation toolchains from high-level machine learning model specifications to specialized accelerators. The internship work will involve the design of programming abstractions, optimizations, static analyses, and code generation. Knowledge of machine learning and neural network concepts is desirable but not a prerequisite. Candidates with experience in programming languages and compilers – especially domain-specific languages and optimizations for linear algebra – are particularly welcome to apply.

Compilers

Automatic generation of peephole optimizers from specifications

Supervisor: Nuno Lopes

Start Date: May 2018 or earlier

Applications close January 19, 2018

Reference #: MSRC225

The compilation time of modern compilers is often dominated by DAG rewriters. These rewriters are implemented by hand and often rely on side static analysis to discharge preconditions of rewrite rules.

The intern will explore ways to automatically generate DAG rewriters from specifications written in the Alive DSL, with the goals of 1) make optimizations faster, 2) ensure they are correct by construction, and 3) reduce implementation time of new rewrite rules. The final tool should be able to produce high-performance C++ code that can be included directly into LLVM/MSVC/etc (to replace e.g., LLVM’s InstCombine/InstSimplify).The main research question is how to share the matching of patterns in the most efficient way (through automata-based techniques) to gain performance, and how to avoid doing multiple passes over the IR until fixed-point like current optimizers do.

No experience in compilers required.

Please contact nlopes@microsoft.com directly.

Security

Azure Confidential Computing

Supervisor: Manuel Costa, Olya Ohrimenko, Felix Schuster

Start Date: June 2018

Applications close: January 31, 2018

Reference #: MSRC234

Hardware-rooted trusted execution environments (TEEs), such as Intel SGX, enable isolated execution of sensitive workloads. For instance, Microsoft Azure recently announced the availability of SGX-enabled hardware in its data centers. Our team works on the design of secure applications based on TEEs and tools for hardening the code running inside TEEs. Recently, we worked on blockchain applications based on TEEs and countermeasures for side-channel attacks.We are looking for two interns, ideally with a background in systems security, side-channel attacks, and defenses, compilers, formal verification, or blockchains.

Our project page: http://approjects.co.za/?big=en-us/research/project/trusted-cloud/

Azure Confidential Computing: https://azure.microsoft.com/en-us/blog/introducing-azure-confidential-computing/ 

Privacy

Confidential Machine Learning

Supervisor: Olya Ohrimenko

Start Date: Beginning of April 2018 or earlier

Applications close: January 15, 2018

Reference #: MSRC235

Multi-party machine learning raises concerns from individual parties with regards to privacy of the data they contribute. In this project, we want to investigate privacy definitions and techniques as they apply to machine learning algorithms. We are looking for candidates interested in the topics of privacy-preserving and robust machine learning and data analysis, in general, including differential privacy.

Our project page: http://approjects.co.za/?big=en-us/research/project/trusted-cloud