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.



Established: June 1, 2013

Tabular is a Excel add-in that brings the power of model based machine learning to data enthusiasts. It allows the user to write a simple model that explains their data and perform Bayesian inference. Tabular is built on top of Infer.NET. Tabular is a probabilistic programming language that brings the power of machine learning to data enthusiasts — the large class of spreadsheet users who wish to model and learn from their…

Infer.NET Fun

Established: April 2, 2012

"I think it's extraordinarily important that we in computer science keep fun in computing." Alan J. Perlis - ACM Turing Award Winner 1966. Infer.NET Fun turns the simple succinct syntax of F# into an executable modeling language for Bayesian machine learning. We propose a marriage of probabilistic functional programming with Bayesian reasoning. Infer.NET Fun turns F# into a probabilistic modeling language – you can code up the conditional probability distributions of Bayes’ rule using…

University of Edinburgh Microsoft Research Joint Initiative in Informatics

Established: October 5, 2011

The joint initiative celebrates and consolidates research ties between the School of Informatics of the University of Edinburgh, and Microsoft Research, through the annual award of studentships to up to four PhD scholars within the Microsoft Research PhD Scholarship programme. The initiative was launched October 5, 2011, at a meeting between Professor Sir Tim O’Shea, Principal of the University of Edinburgh, and Rick Rashid, Chief Research Officer, Microsoft Research. The convenor of the initiative is Andy Gordon,…

F7: Refinement Types for F#

Established: May 29, 2008

F7 is an enhanced typechecker for the F# programming language, a dialect of ML. F7 pioneers the static checking of security properties expressed with refinement types. Although the original motivation was to check security properties, F7 is not security-specific and is applied in other areas, such as database modelling. The theoretical core of F7 is the typed lambda-calculus Refined Concurrent FPC, or RCF for short. FPC itself is Plotkin and Gunter's lambda-calculus with function, sum,…

Samoa: Formal Tools for Securing Web Services

Established: May 16, 2003

An XML web service is, to a first approximation, a wide-area RPC service in which requests and responses are encoded in XML as SOAP envelopes, and transported over HTTP. Applications exist on the internet (for programmatic access to search engines and retail), on intranets (for enterprise systems integration), and are emerging between intranets (for the e-science Grid and for e-business). Specifications (such as WS-Security, now at OASIS) and early toolkits (such as Microsoft's WSE product)…









Code-Carrying Authorization
Sergio Maffeis, Martín Abadi, Cédric Fournet, Andy Gordon, in 13th European Symposium on Research in Computer Security, Málaga, Spain, October 6-8, 2008. Proceedings, Springer Berlin Heidelberg, October 6, 2008, View abstract, Download PDF













Concurrent Haskell
Simon Peyton Jones, Andy Gordon, Sigbjorn Finne, in POPL '96 Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ACM Press, January 21, 1996, View abstract, Download PDF






Link description

Verified Computing Tools


April 14, 2011


Andy Gordon, Bart Jacobs, and Markus Dahlweid


MSR Cambridge, Katholieke Universiteit Leuven, European Microsoft Innovation Center


Infer.NET Fun: An F# Library for Probabilistic Programming

March 2012

    Click the icon to access this download

  • Website

F7: Refinement Types for F# (2012)

November 2011

    Click the icon to access this download

  • Website

WSE Policy Advisor

March 2005

    Click the icon to access this download

  • Website


July 2002

    Click the icon to access this download

  • Website