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.
ACM Fellow in 2020