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. Since April 2007, I am
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’m giving a series of lectures in 2009 on the Principles and Applications of Refinement Types.
Research. My interests are in the general area of computer programming languages. I've published and lectured on operational semantics, type theory, concurrency theory, automated reasoning, program logics, and functional and object-oriented programming. 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 security-enhanced typechecker for F#.
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’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.
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![]()
![]()