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.
	Tools  We are home 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.
	Systems biology We focus on the design and analysis of executable programs describing biological phenomena, DNA computing, and molecular programming.

Recent news

• Source code release of T2 now available! [download]
• Andrey Rybalchenko joins the team! [more]
• Welcome to our latest PPT interns: Thomas Stroder and Aws Albarghouthi!
• Matthew Parkinson is this year's recipient of the 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 recently in Nature [more]

Playground

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

• Try F#
• SLAyer
• F*
• BMA

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 Byron Cook, Andy Gordon or any member of the team.

Contact Us

• Programming Principles
  and Tools Research Group
  Microsoft Research
  21 Station Road
  Cambridge CB1 2FB, UK
  +44 1223 479700