AndrewDGordon

Andrew D. Gordon

Andrew D. Gordon is a computer scientist specializing in formal methods, AI, and programming languages.

As Science Advisor at the Advanced Research + Invention Agency (ARIA), Andy advises the Safeguarded AI programme on cybersecurity, AI, and formal methods. As Science Advisor at Cogna, Andy leads research on delivering software from natural language, including DSL design, finding ambiguities in specifications, and testing and verification of AI-generated applications with various formal methods.

Before joining Cogna as an early employee in 2023, Andy had a 26 year career at Microsoft Research. As Partner Research Manager, Andy led a diverse team of researchers and engineers to evolve Excel as an end-user programming language. He made significant contributions to the development of natural language formulas using generative AI in Copilot for Excel, formula features like LET/LAMBDA, the Calc.ts client-side execution engine for Excel formulas, and Excel Labs.

Andy was recognised as a 2020 Fellow of the Association for Computing Machinery (ACM) for his research on programming languages: their principles, logic, usability, and trustworthiness.

Andy is now Honorary Professor at the University of Edinburgh, following 12 years as full Professor. His PhD research at Cambridge contributed to the design of monadic I/O in Haskell, with his ASCII art “»=” inspiring the Haskell logo. During his postdoc at Chalmers University he pioneered the use of the locally nameless representation in formal proofs.

Selected Publications

  1. Richard J. Boulton, Andrew D. Gordon, Michael J. C. Gordon, John Harrison, John Herbert, John Van Tassel: Experience with Embedding Hardware Description Languages in HOL. TPCD 1992: 129-156.
  2. Andrew D. Gordon: Functional Programming and Input/Output. University of Cambridge, 1992. Published as book by Cambridge University Press, 1994.
  3. Andrew D. Gordon: A Mechanisation of Name-Carrying Syntax up to Alpha-Conversion. HUG 1993: 413-425.
  4. Simon L. Peyton Jones, Andrew D. Gordon, Sigbjørn Finne: Concurrent Haskell. POPL 1996: 295-308.
  5. Martín Abadi, Andrew D. Gordon: A Calculus for Cryptographic Protocols: The Spi Calculus. Inf. Comput. 148(1): 1-70 (1999).
  6. Luca Cardelli, Andrew D. Gordon: Mobile Ambients. Theor. Comput. Sci. 240(1): 177-213 (2000).
  7. Luca Cardelli, Andrew D. Gordon: Anytime, Anywhere: Modal Logics for Mobile Ambients. POPL 2000: 365-377.
  8. Andrew D. Gordon, Don Syme: Typing a Multi-Language Intermediate Code. POPL 2001: 248-260.
  9. Andrew D. Gordon, Alan Jeffrey: Authenticity by Typing for Security Protocols. J. Comput. Secur. 11(4): 451-520 (2003).
  10. Moritz Y. Becker, Cédric Fournet, Andrew D. Gordon: SecPAL: Design and Semantics of a Decentralized Authorization Language. J. Comput. Secur. 18(4): 619-665 (2010).
  11. Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Sergio Maffeis: Refinement Types for Secure Implementations. ACM Trans. Program. Lang. Syst. 33(2): 8:1-8:45 (2011).
  12. Gavin M. Bierman, Andrew D. Gordon, Catalin Hritcu, David E. Langworthy: Semantic Subtyping with an SMT Solver. J. Funct. Program. 22(1): 31-105 (2012).
  13. Sooraj Bhat, Johannes Borgström, Andrew D. Gordon, Claudio V. Russo: Deriving Probability Density Functions from Probabilistic Functional Programs. TACAS 2013: 508-522.
  14. Andrew D. Gordon, Thomas A. Henzinger, Aditya V. Nori, Sriram K. Rajamani: Probabilistic Programming. FOSE 2014: 167-181.
  15. Andrew D. Gordon, Thore Graepel, Nicolas Rolland, Claudio V. Russo, Johannes Borgström, John Guiver: Tabular: A Schema-Driven Probabilistic Programming Language. POPL 2014: 321-334.
  16. Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, Marcin Szymczak: A Lambda-Calculus Foundation for Universal Probabilistic Programming. ICFP 2016: 33-46.
  17. Maria I. Gorinova, Andrew D. Gordon, Charles Sutton: Probabilistic Programming with Densities in SlicStan: Efficient, Flexible, and Deterministic. Proc. ACM Program. Lang. 3(POPL): 35:1-35:30 (2019).
  18. Matt McCutchen, Judith Borghouts, Andrew D. Gordon, Simon Peyton Jones, Advait Sarkar: Elastic Sheet-Defined Functions: Generalising Spreadsheet Functions to Variable-Size Input Arrays. J. Funct. Program. 30: e26 (2020).
  19. Michael Xieyang Liu, Advait Sarkar, Carina Negreanu, Benjamin G. Zorn, Jack Williams, Neil Toronto, Andrew D. Gordon: “What It Wants Me To Say”: Bridging the Abstraction Gap Between End-User Programmers and Code-Generating Large Language Models. CHI 2023: 598:1-598:31.
  20. Diana Robinson, Christian Cabrera, Andrew D. Gordon, Neil D. Lawrence, Lars Mennen: Requirements Are All You Need: The Final Frontier for End-User Software Engineering. ACM Transactions on Software Engineering and Methodology, 34(5): 1-22 (2025).