Amal Ahmed
(she/her/hers)
Professor
Research interests
- Programming languages
- Correct and secure compilation
- Gradual typing
- Safe language interoperability
Education
- PhD in Computer Science, Princeton University
- MS in Computer Science, Stanford University
- BA in Computer Science and Economics, Brown University
Biography
Amal Ahmed is a professor in the Khoury College of Computer Sciences at Northeastern University, based in Boston.
Ahmed's research involves programming languages and compiler verification with a focus on type systems, semantics, secure compilation, gradual typing, and software contracts. Her work scaling the logical relations proof method to realistic languages with various features was widely used for the correctness of compiler transformations, soundness of advanced type systems, and verification of fine-grained concurrent data structures. Ahmed also developed the first proof architecture for verifying multi-pass compilers in the presence of inter-language linking of compiled code.
Ahmed has served on numerous program committees in her field of programming languages, including ACM SIGPLAN Symposium on Principles of Programming Languages, ACM SIGPLAN International Conference on Functional Programming, IEEE Symposium on Logic in Computer Science, and the European Symposium on Programming. She has been a regular invited lecturer at the annual Oregon Programming Languages Summer School 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 ACM SIGPLAN International Conference on Functional Programming, Programming Languages Mentoring Workshop, and ACM SIGPLAN Workshop on Types in Language Design and Implementation. Her earned honors include an NSF Career Award, a Google Faculty Research Award, and a George Van Ness Lothrop Fellowship.
Before joining Northeastern, Ahmed was an assistant professor at Indiana University for three years, a research assistant professor at the Toyota Technological Institute at Chicago for three years, and a postdoctoral fellow at Harvard University for two years.
Labs and groups
Recent publications
-
Realistic Realizability: Specifying ABIs You Can Count On
Citation: Andrew Wagner, Zachary Eisbach, Amal Ahmed . (2024). Realistic Realizability: Specifying ABIs You Can Count On Proc. ACM Program. Lang., 8, 1249-1278. https://doi.org/10.1145/3689755 -
RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly
Citation: Zoe Paraskevopoulou, Michael Fitzgibbons, Michelle Thalakottur, Noble Mushtak, Jose Sulaiman Mazur, Amal Ahmed . (2024). RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly CoRR, abs/2401.08287. https://doi.org/10.48550/arXiv.2401.08287 -
Semantic Encapsulation using Linking Types
Citation: Daniel Patterson , Andrew Wagner, Amal Ahmed . (2023). Semantic Encapsulation using Linking Types TyDe@ICFP, 14-28. https://doi.org/10.1145/3609027.3609405 -
Lilac: a Modal Separation Logic for Conditional Probability
Citation: John M. Li, Amal Ahmed , Steven Holtzen. (2023). Lilac: a Modal Separation Logic for Conditional Probability CoRR, abs/2304.01339. https://doi.org/10.48550/arXiv.2304.01339 -
Semantic soundness for language interoperability
Citation: Daniel Patterson , Noble Mushtak, Andrew Wagner, Amal Ahmed . (2022). Semantic soundness for language interoperability PLDI, 609-624. https://doi.org/10.1145/3519939.3523703 -
ANF preserves dependent types up to extensional equality
Citation: Paulette Koronkevich, Ramon Rakow, Amal Ahmed , William J. Bowman. (2022). ANF preserves dependent types up to extensional equality J. Funct. Program., 32, e12. https://doi.org/10.1017/S0956796822000090 -
Typed closure conversion for the calculus of constructions
Citation: William J. Bowman, Amal Ahmed . (2018). Typed closure conversion for the calculus of constructions PLDI, 797-811. https://doi.org/10.1145/3192366.3192372