I am a Principal Research Manager at Microsoft Research, Cambridge.
My main project is Calc Intelligence, bringing intelligence to end-user programming, especially spreadsheets.
Grad students, if you are interested in working on spreadsheet experience and technology, get in touch.
As a part-time position, I also hold the Chair in Computer Security and am a member of the Laboratory for Foundations of Computer Science and the Security and Privacy group in the School of Informatics in the University of Edinburgh. I convene the University of Edinburgh Microsoft Research Joint Initiative in Informatics. I participate in the Data Science PhD programme and the Cyber Security & Privacy Research Network.
Between April 2007 and April 2010, I was a Visiting Professor in the School of Computing Science at the University of Newcastle upon Tyne.
My research is on programming languages and their semantics and logics, with application to security and privacy, machine learning, concurrency, and databases. I’ve published and lectured on: input/output in pure functional programming; hardware description languages; mobile computation; security protocols; web services security; distributed authorization; configuration management; and database programming languages.
I have worked on probabilistic programming for machine learning.
I am the co-inventor of two popular formalisms for describing concurrent processes: the spi calculus (with M. Abadi) and the ambient calculus (with L. Cardelli).
One project is an analysis (with D. Syme) of the type system underlying the bytecode verifier of the Microsoft .NET Common Language Runtime.
Another is Cryptyc (with A. Jeffrey), a type-checker for cryptographic protocols.
The Samoa Project developed formal tools for the security of XML Web Services.
CVK, the Crypto Verification Toolkit, is a suite of tools for verifying security properties of cryptographic protocols and APIs in F#; the latest member of CVK is F7, a refinement-type checker for F#.
Dminor is an enhanced typechecker – based on semantic subtyping – for the SQL Server Modeling Language “M”. I gave a series of lectures in 2009 on the Principles and Applications of Refinement Types.
The Csec Project is developing verification techniques for cryptographic software in C.
I have a profile at ResearchR.org.
I am listed on the Edinburgh Research Explorer.