Programming Principles and Tools

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

  • Congratulations to Manuel Costa who has been awarded the Eurosys Jochen Liedtke Young Researcher Award at the Eurosys Conference.
  • 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

  • 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 Openness.  Cedric 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]

People

Follow us:

Share this page: