The 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:
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.
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.
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]
We focus on the design and analysis of executable programs describing biological phenomena, DNA computing, and molecular programming.
Welcome to our latest PPT interns: Marc Andrysco, and Julia Kramer.
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.
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.
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 Openness. Cedric got interviewed for The Register too. Further information can be found on the project website here.
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.
You’re welcome to play with some of our work in your browser!
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
Andrew J. Lilly,
Adam C. Wilkinson,
Iain C. Macaulay,
Fabian J. Theis,
The 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: Programming principles We develop new ways to write, structure and reason about programs running […]
Venue: SERC Auditorium, Indian Institute of Science, Bangalore INDIA. 2012 Summer School Program Committee R. Govindarajan, Indian Institute of Science S. Sudarshan, IIT Bombay Chandu Thekkath, Microsoft Research Silicon Valley Ganesan Ramalingam, Microsoft Research India
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…
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…
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…
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…
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…
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…
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…
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.…
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…
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…
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…
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…
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…
Microsoft Research Blog
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.
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.