Portrait of Andy Gordon

Andy Gordon

Principal Researcher


I am a Principal Researcher at Microsoft Research, Cambridge, where I manage Programming Principles and Tools.

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.

Before joining Microsoft in 1997, I was a Royal Society University Research Fellow at the University of Cambridge Computer Laboratory.

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.

  • My current research is 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.

My publications are listed here on my Publications tab, in addition to DBLPGoogle Scholar, and some on arXiv.

I have a profile at ResearchR.org.

I am listed on the Edinburgh Research Explorer.