Portrait of Andy Gordon

Andy Gordon

Principal Researcher

About

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.

Projects

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…

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…

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…

Publications

2014

2013

2012

2011

2010

2009

2008

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

2007

2006

2005

2004

2003

2002

2001

2000

1999

1998

1997

1996

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

1995

1994

1993

1992

Projects

Verified Computing Tools Link description

Verified Computing Tools

Date

April 14, 2011

Speakers

Andy Gordon, Bart Jacobs, and Markus Dahlweid

Affiliation

MSR Cambridge, Katholieke Universiteit Leuven, European Microsoft Innovation Center