Programming Principles and Tools

Established: March 27, 2000

Programming Principles and ToolsThe Programming Principles and Tools group devises formal techniques and models for understanding programs, programming abstractions and languages, and develops related implementation technology. Programming Principles and Tools is part of Microsoft Research Cambridge.

Our work can be grouped into four themes:

ppt-2Programming principles
We develop new ways to write, structure and reason about programs running in various environments. This includes advanced type and module systems, logics and semantic models, and probabilistic programming for machine learning.

toolsTools
We contribute to the Haskell and F# programming languages. We have a strong interest in the Coq theorem prover. We build world-class verification tools as well as tools for modelling various biological systems.

ppt-4Constructive security
We work on various security and privacy issues surrounding programming, applications and systemms, seeking robust solutions to real-world large-scale security and privacy problems. [more]

ppt-5Systems biology
We focus on the design and analysis of executable programs describing biological phenomena, DNA computing, and molecular programming.

 

Recent News

  • Welcome to our latest PPT interns:
  • Welcome to Sylvan Clebsch and Pantazis Deligiannis who have both joined PPT as an RSDE.  Sylvan and Pantazis are formerly from Imperial College London.
  • Welcome to Steven Woodhouse who has joined PPT as a Post Doc Researcher and Felienne Hermans from Delft University of Technology who has joined us as a Visiting Researcher.
  • Congratulations to Samin Ishtiaq on winning the 2016 CAV Award for work on heap analysis via SLAyer.
  • Jasmin Fisher has been elected a Fellow of Trinity College in Cambridge.
  • Mikolas Janota participated with his solvers for Quantified Boolean Formulas (ABFs) in the QBF-Eval – a QBF competition and has received several awards but most importantly – Prenex CNF Track, First Place, Solver: bloqqer-RAReQS and 2QBF Track, First Place, Solver: AREQS.
  • Congratulations to Don Syme and Tomas Petricek who received a Distinguished Paper Award at PLDI 2016 for the paper Types from data: Making structured data first-class citizens in F#’.
  • Welcome to Neil Toronto who has joined PPT as a Research Software Engineer.  Neil previously worked as a Postdoctoral Researcher at University of Maryland, USA.
  • Simon Peyton Jones has been elected a Fellow of the Royal Society (FRS)

Playground

You’re welcome to play with some of our work in your browser!

Careers

The Programming Principles and Tools group is always looking for Interns and Post-docs. We are also interested to hear from outstanding researchers and especially recent PhDs. For further information please contact Andy Gordon or any member of the team.

Programming Principlesand Tools Research GroupMicrosoft Research21 Station RoadCambridge CB1 2FB, UK+44 1223 479700

People

Publications

2017

Bringing LTL Model Checking to Biologists
Zara Ahmed, David Benque, Sergey Berezin, Jasmin Fisher, Anna Caroline E. Dahl, Benjamin A. Hall, Samin Ishtiaq, Jay Nanavati, Nir Piterman, Maik Riechert, Nikita Skoblov, in Verification, Model Checking and Abstract Interpretation (VMCAI), Springer, January 15, 2017, View abstract, Download PDF

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

Shape Analysis by Graph Decomposition
G. Ramalingam, Josh Berdine, Byron Cook, in Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings, Springer Verlag, January 1, 2007, View abstract, Download PDF

2006

2005

2004

2003

2002

2001

2000

1999

Downloads

Decomposition-SAT

April 2014

A decomposition-based parallel SAT solver that decomposes SAT formulas efficiently and reconciles solutions between partitions by means of propositional (Craig) interpolation.

    Click the icon to access this download

  • Website

Videos

Events

Microsoft Distinguished Research Lecture: Laws of Programming with Concurrency

Cambridge | January 2015

The basic Laws of Nature sought by many branches of science, as well as the basic axioms postulated in many branches of mathematics, have historically been expressed in great generality as algebraic equations, or occasionally as inequalities. Nowadays these equations provide the theoretical foundation for the design of automated tools which are widely used to help scientists and engineers in pursuit of their goals. This is the way in which Isaac Newton still contributes to…

SEIF Day 2014

Redmond, WA, US | July 2014

The annual Software Engineering Innovation Foundation (SEIF) Day brought together SEIF winners, influential software engineering researchers, and researchers from Microsoft Research to present and discuss existing software engineering projects being pursued by the SEIF community, and future directions in software engineering research.       Organization

MSR India 2012 Summer School on Distributed Algorithms, Systems, and Programming

Bangalore, India | May 2012

The MSR India Summer School series, held in collaboration with the Indian Institute of Science, consists of lectures in a chosen area by leading experts from around the world. The aim is to introduce students and researchers to important new areas and the latest results and to provide a forum for Indian and international researchers to interact. The 2012 Summer School was held between May 28 - June 08 at the Indian Institute of Science, Bangalore…

Projects

Project Everest – Verified Secure Implementations of the HTTPS Ecosystem

Established: May 31, 2016

Summary Project Everest aims to build and deploy a verified HTTPS stack. The HTTPS ecosystem (HTTPS and TLS protocols, X.509 public key infrastructure, crypto algorithms) is the foundation on which Internet security is built. Unfortunately, this ecosystem is extremely brittle, with headline-grabbing attacks such as FREAK and LogJam and emergency patches many times a year. Project Everest proposes to solve this problem by constructing a high-performance, standards-compliant, and verified implementation of the full HTTPS ecosystem. We…

Single Cell Network Synthesis

Established: January 4, 2016

The Single Cell Network Synthesis tool (SCNS) is a tool for the reconstruction and analysis of executable models from single-cell gene expression data, which supports easy deployment of computation to the cloud for performance and control via a web-based graphical interface. SCNS can be used for understanding differentiation, developmental, or reprogramming journeys. SCNS takes single-cell qRNA or RNA-sequencing data, and treats expression profiles as binary states, where a value of 1 indicates a gene is expressed and 0 indicates…

Ziria – Wireless Programming for Hardware Dummies

Established: June 16, 2014

Software-defined radios (SDR) have a potential to bring major innovation in wireless networking design. However, their impact so far has been limited due to complex programming tools. Ziria addresses this problem. It consists of a novel programming language and an optimizing compiler. It is able to synthesize a very efficient SDR code from a high-level PHY description written in Ziria language. Link to code Ziria@GitHub Slides NEW: tutorial slides, covering WiFi case study in Ziria…

Predictive dynamic model of Glioblastoma early development

Established: September 2, 2013

Glioblastoma multiforme (GBM) is the most common and most malignant form of brain cancer, being characterised by relentless growth and aggressive invasion into the healthy brain tissue, resulting in extremely poor outcome. Given the complexity and cell heterogeneity observed in this type of tumour, it is natural to study its development from an integrative and systems perspective. This project aims to develop an executable hybrid model of tumour growth. The model integrates a multi-level description…

Whole-organism model of C. elegans development

Established: January 6, 2013

The nematode C. elegans, with its invariant lineage, serves as a model organism for the study of development. We aim to create an open-source, extensible whole-organism model of C. elegans development to which the worm community can add new information. In the first stage of this project we use this simulation program to study developmental variance in C. elegans, and in particular how this may arise through perturbations in cell-cycle timing. This early version of…

Decoding transcriptional programs of blood cell development

Established: December 3, 2012

Understanding the mechanisms that govern stem cell self-renewal and cell fate decisions are fundamental to regenerative medicine and to understanding how these mechanisms are perturbed in disease states. Blood cell development (haematopoiesis) has long stood as a paradigm for studying stem cell biology. Genes encoding transcriptional regulators and components of cell signalling pathways are recognised as powerful regulators of developmental processes including the development of blood cells. The interplay of sensing the external environment (through…

Mechanisms of stem cell homeostasis during C. elegans germline development

Established: October 1, 2012

The establishment of homeostasis between cell growth, differentiation and apoptosis is of key importance for organogenesis. Stem cells respond to temporally and spatially regulated signals by switching from mitotic proliferation to asymmetric cell division and differentiation. Executable computer models of signalling pathways can accurately reproduce a wide range of biological phenomena by reducing detailed chemical kinetics to a discrete, finite form. Moreover, coordinated cell movements and physical cell-cell interactions are required for the formation of…

The executable path to Myc

Established: August 6, 2012

Myc is a key oncogene in various cancers occurring across a diverse range of tissues. In order to better understand and treat these cancers, it is vital that we understand how the opposing functions of Myc, proliferation and apoptosis, are balanced and regulated in healthy tissue, and how this goes wrong in cancer. In collaboration with the Evan lab (Department of Biochemistry, University of Cambridge) we aim to build comprehensive executable models of the Myc…

Executable network models to identify new treatment combinations for leukaemia

Established: June 4, 2012

Chronic Myeloid Leukemia (CML) represents a paradigm for the wider cancer field. Despite the fact that tyrosine kinase inhibitors have established targeted molecular therapy in CML, patients often face the risk of developing drug resistance, caused by mutations and/or activation of alternative cellular pathways. To optimize drug development, one needs to systematically test all possible combinations of drug targets within the genetic network that regulates the disease. We previously built a CML network-model using BMA,…

University of Edinburgh Microsoft Research Joint Initiative in Informatics

The joint initiative celebrates and consolidates research ties between the School of Informatics of the University of Edinburgh, and Microsoft Research, through the annual award of studentships to up to four PhD scholars within the Microsoft Research PhD Scholarship programme. The initiative was launched October 5, 2011, at a meeting between Professor Sir Tim O’Shea, Principal of the University of Edinburgh, and Rick Rashid, Chief Research Officer, Microsoft Research. The convenor of the initiative is Andy Gordon,…

Privacy-friendly smart metering

Many smart metering proposals threaten users' privacy by disclosing fine-grained consumption data to utilities. We have designed protocols that allow for precise billing of consumption while not revealing any consumption information to third parties. We also have developped protocols that allow for privacy-friendly real-time aggregation of smart-meter readings. Information computed on the basis of fine-grained smart-meter readings has multiple uses within the energy industry, including billing, providing energy advice, settlement,…

F7: Refinement Types for F#

Established: May 29, 2008

F7 is an enhanced typechecker for the F# programming language, a dialect of ML. F7 pioneers the static checking of security properties expressed with refinement types. Although the original motivation was to check security properties, F7 is not security-specific and is applied in other areas, such as database modelling. The theoretical core of F7 is the typed lambda-calculus Refined Concurrent FPC, or RCF for short. FPC itself is Plotkin and Gunter's lambda-calculus with function, sum,…

Posts

Cardelli Receives 2007 Senior Dahl-Nygaard Prize

By Rob Knies, Managing Editor, Microsoft Research Luca Cardelli, a principal researcher at Microsoft Research Cambridge, has been named winner of the 2007 Senior Dahl-Nygaard Prize, presented annually to a senior researcher with outstanding career contributions. Cardelli, who heads the Programming Principles and Tools team at the Cambridge lab, was cited for his overall contribution to both theory and practice for object-oriented languages. The prize was award in Berlin on Aug. 2 during the 21st…

August 2007

Microsoft Research Blog

Computing Industry Bestows Rare Honor upon Hoare, Lampson

By Rob Knies, Managing Editor, Microsoft Research One has spent his professional career exploring programming language theory. The other has made fundamental contributions to PC networks, operating systems, security, and document publishing. One works in Cambridge, U.K. The other works in Cambridge, Mass. But Tony Hoare and Butler Lampson have a couple of things in common: Both work for Microsoft Research, and both were named fellows of the Computer History Museum during an awards dinner…

October 2006

Microsoft Research Blog

News archive

  • Congratulations to Cedric Fournet and Markulf Kohlweiss who received the Levchin Prize, provided by internet entrepreneur Max Levchin, at the Real World Cryptography Conference.
  • The open-source release of miTLS happened during the last Open Source Summit in Paris on 18 November 2015.  This featured in Next at Microsoft and OpennessCedric got interviewed for The Register too.  Further information can be found on the project website here.
  • Luca Cardelli has been awarded the 2015 ACM SIGPLAN Programming Languages Achievement Award.
  • Congratulations to Santiago Zanella-Beguelin who received a Best Paper Award at ACM CCS on 12 October 2015.  The paper ‘Imperfect Forward Secrecy: How Diffie-Hellman Fails In Practice’ can be found here.  The official announcement can be found on the ACM website but mistakenly listed as Best Student Paper Award.  The paper also got a Pwnie Award for Most Innovative Research at BlackHat 2015 on 3 August 2015.
  • Congratulations to Cedric Fournet and Markulf Kohlweiss, and their INRIA colleagues for a distinguished paper award at IEEE Security and Privacy, Oakland.  The paper “A Messy State of the Union: Taming the Composite State Machines of TLS” is on testing implementations of TLS using a test harness built over their reference implementation miTLS, which led to their discovery of the FREAK attack on TLS.
  • Cedric Fournet and Markulf Kohlweiss make it into the The Register for producing Geppetto.
  • F# 4.0 has been released in Visual Studio 2015 community preview releases. F# is open source and cross-platform. Our group contribute to F#, and the language designer is Don Syme, a researcher in our group.
  • F# type providers and cloud programming featured at dotnetconf Microsoft’s online conference for .NET. Using research results from our group, collaborators Tomas Petricek (fsharpWorks) and Isaac Abraham (elastacloud) presented this joint work with Don Syme on 19 March 2015 in an online presentation from Skype HQ, London.
  • On 19 November 2014, Tony Hoare was awarded an Honorary Prize Fellowship of the Cambridge Philosophical Society. He gave a well attended lecture, addressing the question ‘Can Computers Understand their Own Programs?’. His positive answer was supported by a survey of ideas derived from Aristotle, Euclid, and Alan Turing.
  • Andrey Rybalchenko and Nuno Lopes have been awarded the HVC’14 Award for a PLDI’12 paper “Synthesizing Software Verifiers from Proof Rules [more]
  • Ben Hall has been awarded the prestigious Royal Society University Research Fellowship [more]
  • Together with external collaborators Christoph Wintersteiger received the IJCAR 2014 Best Paper Award together [more]
  • Ben Hall’s work on modelling safety valves in neurons has just appeared in Nature Communications [more]
  • T2 Temporal Prover now open source[download] [more]
  • Matthew Parkinson is the recipient of the 2013 Dahl-Nygaard prize [more]
  • Georges Gonthier recently completed an historic computer-assisted proof of the Feit-Thompson Theorem [more]
  • Jasmin Fisher‘s work on modelling cancer cells was featured in Nature [more]