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 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.
|Constructive security |
We work on various security and privacy issues surrounding programming, applications and systems. [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: Siddarth Krishna, Miguel Neves, Alex Horn, Henning Gunther, Matthias Schlaipfer
- 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 in an online presentation from Skype HQ, London.
- Welcome to Aditya Nori who has just joined us from MSR India and James Lingard who has moved from the Systems & Networking Group.
- The deadline for post-doc applications is January 5, 2015. Please allow a few days for your referees to upload their letters.
- 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]
- Programming Principles
and Tools Research Group
21 Station Road
Cambridge CB1 2FB, UK
+44 1223 479700