I'm a Principal Researcher
with Microsoft Research, Cambridge, in the Programming
Principles and Tools group. 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, and I have a blog.�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 is developing 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 ��/a>.
Professional activities. I am chairing 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� 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.
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.
Some recent and upcoming events:
Andrew Gordon, adgXmicrosoft.com where X=@
Microsoft Research![]()
![]()