Andrew D.
Gordon
I
am a Principal Researcher with Microsoft
Research, Cambridge, in the Programming
Principles and Tools and Security
groups.
I
also hold the Chair
in Computer Security and am a member of the Laboratory for Foundations of Computer
Science in the School of
Informatics in the University of
Edinburgh. I convene the University of
Edinburgh Microsoft Research Joint Initiative in Informatics.
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.
Online material. A separate page lists my publications and another gives full details. Other pages contain some research talks and some teaching-related materials. I gave a series of lectures in 2009 on the Principles and Applications of Refinement Types. My publications are listed at DBLP, Google Scholar, and Microsoft Academic Search.
Research. My research is on programming languages and their semantics and logics, with application to security, 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 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). My work focuses on applying type theory and other formal techniques to problems of computer security. 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”. The Csec Project is developing verification techniques for cryptographic software in C.
Professional activities. I chaired the PC for ESOP 2010, part of ETAPS 2010 in Paphos; previously, I co-chaired the FMSE 2006 PC and chaired the FOSSACS 2003 PC, part of ETAPS 2003 in Warsaw. I serve on the ETAPS steering committee, the Scientific Advisory Board of the Excellence Cluster on Multimodal Computing and Interaction in Saarbruecken, the UK Computing Research Committee, the EPSRC peer review college (2006-2009), and the Editorial Board of Logical Methods in Computer Science; I’m a former member of the MyThS Advisory Board. I co-founded the HOOTS series of workshops on Higher Order Operational Techniques in Semantics, held in Cambridge, Stanford, Paris, and Montreal, and co-edited the HOOTS book.
Open research positions at MSR Cambridge. We are hiring. The main round of interviews each year is around March and April, with applications due by the end of February. Still, we welcome applications at any time of the year; to apply you should contact me (or another researcher) and fill in the online application form.
Summer internships at MSR Cambridge. I welcome applications for
summer internships; the deadline each year is the end of February. These
are 12 week research projects, undertaken here at MSR Cambridge, typically by
grad students mid-way through their PhD. There 
is
an online
application form.
Working environment. Having affiliations with both Microsoft
Research and the University of Edinburgh, I am fortunate to have two sets of
excellent colleagues in the two ancient and beautiful cities, Cambridge and
Edinburgh.
Our
offices are in two modern research buildings, the Roger Needham
building (named after a pioneer in computer security, the first managing
director of MSR Cambridge, and one of my mentors), and the Informatics
Forum (the award-winning home to Edinburgh’s School of Informatics, on the
corner of George Square, in the heart of the city).
Some recent and upcoming events:
- Joint HP-MSR Research Workshop on The Rise and Rise of the
Declarative Datacentre, Cambridge, May 12-13, 2008.
- Summer School on the Global Computing Approach to Analysis
of Systems (GLOBAN 2008), Warsaw, September 22-26, 2008.
- Eleventh International Symposium on Practical Aspects of Declarative
Languages (PADL'09), Savannah, Georgia, January 19-20, 2009.
- British
Colloquium for Theoretical Computer Science (BCTCS’09), Warwick, April
6-9, 2009.
- 30th IEEE Symposium on Security and Privacy
(S&P’09), Oakland, California, May 17-20, 2009.
- 22nd IEEE Computer Security
Foundations Symposium (CSF’09), Port Jefferson, New York, July 8-10,
2009.
- European
Symposium on Programming (ESOP’10), Paphos, March 22-26, 2010.
- International Workshop on Relations
and Data Integrity Constraints and Languages (RADICAL 2010),
Cambridge, May 10-11, 2010.
- First
CryptoForma Workshop, Paris, May 25, 2010.
- ACM SIGPLAN Fifth Workshop on Programming
Languages and Analysis for Security (PLAS 2010), Toronto, June 10,
2010.
- SICSA PhD Conference 2011, Edinburgh, May
23-25, 2011. (Photos here
and here.)
- Second
CryptoForma Workshop, Limerick, June 21, 2011.
- 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
(POPL 2012), Philadelphia, January 25-27, 2012.
Andrew Gordon, adgXmicrosoft.com where X=@
Microsoft Research.gif){kind=small}
.gif){kind=small}
