Portrait of Andy Gordon

Andy Gordon

Senior Principal Research Manager

About

Andy Gordon leads Calc Intelligence at Microsoft Research, bringing intelligence to end-user programming, especially spreadsheets. Calc Intelligence partners closely with Microsoft Excel: features such as LAMBDA and Calc.ts, arising from their mission to enhance Excel as a programming language, ship now in production to many millions of customers.

Andy’s research is on programming languages: their principles, logic, usability, and trustworthiness. 

Ideas from his work have had impact on several best-in-class programming languages, including Excel, the world’s most widely used programming language. The idea of refinement types for verifying security-critical code in the F7 typechecker was adopted by F*, a widely used language for verified code. The idea of information-flow levels for probabilistic programs in Tabular, a language for machine learning on spreadsheet tables, has been adapted to Stan, the most widely used probabilistic programming language. The idea of symbolic crypto in process calculus in the spi calculus (with M. Abadi), is a key underpinning for ProVerif, the most widely used language for symbolic verification of crypto protocols. His pioneering papers on process calculi for mobility and security were influential in the research community: his ETAPS 1998 paper on the ambient calculus (with L. Cardelli) is the most widely cited paper ever at ETAPS, the major European research conference on theory and practice of software. His PhD research was on I/O for Haskell: he invented the “>>=” symbol, and served on the Haskell Committee to standardize monadic I/O.

As a research manager for a decade, Andy is passionate about diversity and inclusion.

Andy is Senior Principal Research Manager at Microsoft Research, Cambridge and part-time Professor at the University of Edinburgh.

Awards and Honours

  1. Distinguished Dissertation in Computer Science, Functional Programming and Input/Outputjointly awarded by the British Computer Society and the Conference of Professors and Heads of Computing, 1993. 
  2. Invited Keynote Speaker at IEEE Logic in Computer Science on Provable Implementations of Security Protocols (LICS’06), Seattle, August 2006. 
  3. Most Influential ETAPS 1998 Paper, Mobile Ambients, with L. Cardelli, awarded by the European Association for Programming Languages and Systems, 2007. 
  4. Microsoft award for transfer of SecPAL: Design and semantics of a decentralized authorization language (Journal of Computer Security 2010) technology to Microsoft Vine product, 2009. 
  5. Most Influential ACM POPL 2000 Paper, Anytime, Anywhere: Modal Logics for Mobile Ambients, with L. Cardelli, awarded by ACM SIGPLAN, 2010. 
  6. Best Paper ETAPS 2013, Deriving Probability Density Functions from Probabilistic Functional Programs, with S. Bhat, J. Borgström, and C. Russo, awarded by the European Association for Programming Languages and Systems, 2013.
  7. Unifying Keynote Speaker on Structure and Interpretation of Probabilistic Programs (ETAPS, Eindhoven, April 2016).
  8. Calc.ts in Excel for the web inducted into Microsoft Wall of Fame, July 2020.