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 with many collaborators 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, 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 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 fortunate and privileged to have wonderfully wise women as mentors and managers over his career: Rosemary Candlin, Mary Sheeran, Karen Spärck Jones, Jane Hillston, and Abigail Sellen.

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

Awards and Honours

1. Recognized as a 2020 ACM Fellow, January 2021.
2. Calc.ts in Excel for the web inducted into Microsoft Wall of Fame, July 2020. 
3. Unifying Keynote Speaker on Structure and Interpretation of Probabilistic Programs (ETAPS, Eindhoven, April 2016).
4. 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.
5. Most Influential ACM POPL 2000 Paper, Anytime, Anywhere: Modal Logics for Mobile Ambients, with L. Cardelli, awarded by ACM SIGPLAN, 2010. 
6. 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. 
7. Most Influential ETAPS 1998 Paper, Mobile Ambients, with L. Cardelli, awarded by the European Association for Programming Languages and Systems, 2007. 
8. Invited Keynote Speaker at IEEE Logic in Computer Science on Provable Implementations of Security Protocols (LICS’06), Seattle, August 2006. 
9. Distinguished Dissertation in Computer Science, Functional Programming and Input/Output, jointly awarded by the British Computer Society and the Conference of Professors and Heads of Computing, 1993.