Amal Ahmed

Assistant Professor

Current Research Projects

  • Verified Compilers for a Multi-Language World
    Software systems today consist of components written in different languages (typed and untyped, high-level and low-level), compiled by different compilers to a common target. The next big challenge in compiler verification is how to guarantee correct compilation while accommodating multi-language software—i.e., without imposing restrictions on linking as existing verified compilers do. Prof. Ahmed’s group is developing a framework for verifying correct compilation of components while ensuring safe linking, even with code compiled from less precisely typed or assembly-like languages.
  • Secure Compilation of Advanced Languages
    Richly typed languages such as Haskell, Coq, and Agda allow programmers to verify code properties from information-flow security to full functional correctness. After compilation, however, these components are run in target-language contexts capable of launching attacks that are not possible in the source language. Prof. Ahmed’s group is working on secure compilation—also known as fully abstract compilation—which guarantees that all security and correctness properties verified at source level still hold at the target level.

Research Interests

Programming languages, particularly semantics and type systems for reasoning about imperative code, concurrency, security, compiler transformations, and provenance. Current focus is on correct and secure compilation, gradual typing, and safe language interoperability.


  • AB in Computer Science and Economics | Brown University
  • MS in Computer Science | Stanford University
  • PhD in Computer Science | Princeton University


Amal Ahmed is an Assistant Professor of Computer Science at Northeastern. Prior to joining Northeastern, she was an Assistant Professor at the School of Informatics and Computing at Indiana University (2009-2011), a Research Assistant Professor at the Toyota Technological Institute at Chicago (2006-2009), and a Postdoctoral Fellow at Harvard University (2004-2006). She received her PhD from Princeton University in 2004.

Professor Ahmed’s research involves programming languages and compiler verification with a focus on type systems, semantics, secure compilation, gradual typing, and software contracts. She is known for her work on scaling the logical relations proof method to realistic languages—with features like memory allocation and mutation, objects, and concurrency—leading to wide use of the technique, e.g., for correctness of compiler transformations, soundness of advanced type systems, and verification of fine-grained concurrent data structures. She recently developed the first proof architecture for verifying multi-pass compilers in the presence of inter-language linking of compiled code.

Professor Ahmed has served on numerous program committees in her field of programming languages, including POPL, ICFP, LICS, and ESOP. She has been a regular invited lecturer at the annual Oregon Programming Languages Summer School (OPLSS) and twice served as co-organizer. She is a member of IFIP WG 2.8 (Working Group on Functional Programming) and has served on the steering committees of ICFP, PLMW, and TLDI. Her awards include an NSF Career Award, a Google Faculty Research Award, and a George Van Ness Lothrop Fellowship.

CCIS Faculty

The brightest and most innovative in the industry