Amal Ahmed

Professor & Associate Dean for Graduate Programs
Khoury College of Computer Sciences
Northeastern University

Ph.D. Computer Science
Princeton University

phone: 617.373.2076
email: amal at ccs.neu.edu
office: 328 West Village H

address:
Northeastern University
Khoury College of Computer Sciences
328 West Village H
440 Huntington Avenue
Boston, MA 02115

Overview

My research interests lie in correct and secure compilation across the software-hardware stack and safe language interoperability, including design of sound foreign-function interfaces (FFIs) and richly typed compiler intermediate languages to support safe mixing of code from different languages. My work makes use of semantics and type systems for reasoning about imperative and probabilistic programming languages, multi-language systems, security, concurrency, compiler correctness, gradual typing, and provenance.

Research Group

I am very fortunate to work with an amazing group! Alumni

Outreach and Education

Professional Activities

Program committees Steering committees
  • PriSC (Jun 2023–present)
  • POPL (Jan 2022–present)
  • SPLASH (Oct 2022–present)
  • ETAPS (Oct 2016–2018)
  • ESOP (Sep 2016–2022)
  • PLMW (Jan 2014–2022), Steering Committee Chair (Jan 2019–Jan 2020)
  • ICFP (Sep 2008–Sep 2012)
  • TLDI (Jan 2009–Oct 2012)

Teaching

  • CS 2500  Fundamentals of CS: Intro to Programming and Computing (F21-Accelerated, F20-Accelerated, F20, F19-Accelerated, F18-Accelerated, F16, S14, F14, F13, F12, F11)
  • CS 7480  Special Topics in PL: Gradual Typing and Principled Language Interoperability (S19)
  • CS 7400  Intensive Principles of Programming Languages (S20 S17, S16, S15)
  • CS 7480  Special Topics in PL: Types, Contracts, Gradual Typing, and Compiler Correctness (F15)
  • CS 4410/6410  Compilers (S13)
  • CS 7480  Special Topics in PL: Type Systems (S12)

Publications

Gradually Typed Languages Should be Vigilant!.
Olek Gierczak, Lucy Menon, Christos Dimoulas, and Amal Ahmed.
Proc. ACM Program. Lang. 8, OOPSLA1, Article 125, 29 pages, Apr 2024.

Semantic Encapsulation Using Linking Types.
Daniel Patterson, Andrew Wagner, and Amal Ahmed.
In ACM SIGPLAN International Workshop on Type-Driven Development (TyDe '23), Seattle, Washington, September 2023.

Lilac: A Modal Separation Logic for Conditional Probability.
John M. Li, Amal Ahmed, and Steven Holtzen.
Proc. ACM Program. Lang. 7(PLDI):148-171 (2023).

ANF Preserves Dependent Types up to Extensional Equality.
Paulette Koronkevich, Ramon Rakow, Amal Ahmed, and William J. Bowman.
Journal of Functional Programming, 32, E22, 2022.

Semantic Soundness for Language Interoperability.
Daniel Patterson, Noble Mushtak, Andrew Wagner, Amal Ahmed.
In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'22), San Diego, California, June 2022.

Gradual Type Theory.
Max S. New, Daniel R. Licata, Amal Ahmed.
Journal of Functional Programming, 31, E21, 2021.

Graduality and Parametricity: Together Again for the First Time.
Max S. New, Dustin Jamner, and Amal Ahmed.
In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL '20), New Orleans, Louisiana, January 2020.
Technical appendix, November 2019.

Under Control: Compositionally Correct Closure Conversion with Mutable State.
Phillip Mates, Jamie Perconti, and Amal Ahmed.
In 21st International Symposium on Principles and Practice of Declarative Programming (PPDP '19), Porto, Portugal, October 2019.

The Next 700 Compiler Correctness Theorems (Functional Pearl).
Daniel Patterson and Amal Ahmed.
In 24th ACM SIGPLAN International Conference on Functional Programming (ICFP '19), Berlin, Germany, August 2019.

Formal Approaches to Secure Compilation: A Survey of Fully Abstract Compilation and Related Work.
Marco Patrignani, Amal Ahmed, and Dave Clarke.
ACM Computing Surveys, 51(6):125.1-125.36, February 2019.
Online Appendix (contains additional sections surveying proof techniques)

Gradual Type Theory.
Max S. New, Daniel R. Licata, and Amal Ahmed.
In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL '19), Lisbon, Portugal, January 2019.

Graduality from Embedding-Projection Pairs.
Max S. New and Amal Ahmed.
In 23rd ACM SIGPLAN International Conference on Functional Programming (ICFP '18), St. Louis, Missouri, September 2018.

Rust Distilled: An Expressive Tower of Languages.
Aaron Weiss, Daniel Patterson, and Amal Ahmed.
At ML Family Workshop (ML '18), St. Louis, Missouri, September 2018.

Typed Closure Conversion for the Calculus of Constructions.
William J. Bowman and Amal Ahmed.
In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '18), Philadelphia, Pennsylvania, June 2018.
Technical Appendix, April 2018.

FabULous Interoperability for ML and a Linear Language.
Gabriel Scherer, Max New, Nick Rioux, and Amal Ahmed.
In 21st International Conference on Foundations of Software Science and Computations Structures (FoSSaCS '18), Thessaloniki, Greece, April 2018.
Full version, April 2018.

Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible.
William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed.
In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL '18), Los Angeles, California, January 2018.
Technical appendix, November 2017.

Correctness of Speculative Optimizations with Dynamic Deoptimization.
Olivier Flückiger, Gabriel Scherer, Ming-ho Yee, Aviral Goel, Amal Ahmed, and Jan Vitek.
In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL '18), Los Angeles, California, January 2018.

Theorems for Free for Free: Parametricity, With and Without Types.
Amal Ahmed, Dustin Jamner, Jeremy Siek, and Philip Wadler.
In 22nd ACM SIGPLAN International Conference on Functional Programming (ICFP '17), Oxford, UK, September 2017.
Technical report, June 2017.

FunTAL: Reasonably Mixing a Functional Language with Assembly.
Daniel Patterson, Jamie Perconti, Christos Dimoulas, and Amal Ahmed.
In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '17), Barcelona, Spain, June 2017.
Technical appendix, April 2017.

Linking Types for Multi-Language Software: Have Your Cake and Eat It Too.
Daniel Patterson and Amal Ahmed.
In SNAPL: Summit on Advances in Programming Languages (SNAPL'17), May 2017.

Fully Abstract Compilation via Universal Embedding.
Max New, William J. Bowman, and Amal Ahmed.
In 21st ACM SIGPLAN International Conference on Functional Programming (ICFP '16), Nara, Japan, September 2016.
Technical appendix, July 2016.

Noninterference for Free.
William J. Bowman and Amal Ahmed.
In 20th ACM SIGPLAN International Conference on Functional Programming (ICFP '15), Vancouver, Canada, September 2015.
Technical appendix, June 2015.

Verified Compilers for a Multi-Language World.
Amal Ahmed.
In SNAPL: Summit on Advances in Programming Languages (SNAPL'15), May 2015.

Database Queries that Explain their Work.
James Cheney, Amal Ahmed, and Umut Acar.
In 16th International Symposium on Principles and Practice of Declarative Programming (PPDP '14), Canterbury, UK, September 2014.

Verifying an Open Compiler Using Multi-Language Semantics.
James T. Perconti and Amal Ahmed.
In 23rd European Symposium on Programming (ESOP '14), Grenoble, France, April 2014.
Technical report, January 2014.

A Core Calculus for Provenance.
Umut Acar, Amal Ahmed, James Cheney, and Roly Perera.
Journal of Computer Security 21(6): 919-969, 2013.
Special issue devoted to selected papers from POST 2012.

Logical Relations for Fine-Grained Concurrency.
Aaron Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, Derek Dreyer.
In 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '13), Rome, Italy, January 2013.
Technical appendix, July 2012.

A Core Calculus for Provenance.
Umut Acar, Amal Ahmed, James Cheney, and Roly Perera.
In 1st Conference on Principles of Security and Trust (POST '12), pp. 410-429, Tallinn, Estonia, March 2012.

An Equivalence-Preserving CPS Translation via Multi-Language Semantics.
Amal Ahmed and Matthias Blume.
In 16th ACM SIGPLAN International Conference on Functional Programming (ICFP '11), pp. 431-444, Tokyo, Japan, September 2011.
Technical appendix, April 2011.

Logical Step-Indexed Logical Relations.
Derek Dreyer, Amal Ahmed, and Lars Birkedal.
Logical Methods in Computer Science (LMCS), 7 (2:16), June 2011.
Special issue devoted to selected papers from LICS 2009.
[ This is a significantly revised and expanded version of our LICS 2009 paper. ]

Blame for All.
Amal Ahmed, Robert Bruce Findler, Jeremy Siek, and Philip Wadler.
In 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '11), pp. 201-214, Austin, Texas, USA, January 2011.

Provenance as Dependency Analysis.
James Cheney, Amal Ahmed, and Umut Acar.
Mathematical Structures in Computer Science (MSCS), 21, pp. 1301-1337, December 2011.
Special Issue on Programming Language Interference and Dependence.

Semantic Foundations for Typed Assembly Languages.
Amal Ahmed, Andrew W. Appel, Christopher Richards, Kedar Swadi, Gang Tan, Daniel Wang.
ACM Transactions on Programming Languages and Systems, 32(3):1-67, March 2010.

Logical Step-Indexed Logical Relations.
Derek Dreyer, Amal Ahmed, and Lars Birkedal.
In 24th Annual IEEE Symposium on Logic in Computer Science (LICS '09), pp. 71-80, Los Angeles, California, USA, August 2009.

Blame for All.
Amal Ahmed, Robert Bruce Findler, Jacob Matthews, and Philip Wadler.
In 1st International Workshop on Script to Program Evolution (STOP '09), Genova, Italy, July 2009.

State-Dependent Representation Independence.
Amal Ahmed, Derek Dreyer, and Andreas Rossberg.
In 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '09), pp. 340-353, Savannah, Georgia, USA, January 2009.
Technical appendix, August 2008.

Typed Closure Conversion Preserves Observational Equivalence.
Amal Ahmed and Matthias Blume.
In 13th ACM SIGPLAN International Conference on Functional Programming (ICFP '08), pp. 157-168, Victoria, British Columbia, Canada, September 2008.
Extended version: Technical Report TR-2008-07, Dept. of Computer Science, University of Chicago, July 2008.

Parametric Polymorphism Through Run-Time Sealing, or, Theorems for Low, Low Prices!
Jacob Matthews and Amal Ahmed.
In 17th European Symposium on Programming (ESOP '08), pp. 16-31, Budapest, Hungary, March 2008.

Imperative Self-Adjusting Computation.
Umut Acar, Amal Ahmed, and Matthias Blume.
In 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '08), pp. 309-322, San Francisco, California, USA, January 2008.
Extended version: Technical Report TR-2007-18, Dept. of Computer Science, University of Chicago, November 2007.

Provenance as Dependency Analysis.
James Cheney, Amal Ahmed, and Umut Acar.
In 11th International Symposium on Database Programming Languages (DBPL '07), pp. 138-152, Vienna, Austria, September 2007.

L3: A Linear Language with Locations.
Amal Ahmed, Matthew Fluet, and Greg Morrisett.
Fundamenta Informaticae, 77(4):397--449, June 2007.

Abstract Predicates and Mutable ADTs in Hoare Type Theory.
Aleksander Nanevski, Amal Ahmed, Greg Morrisett, and Lars Birkedal.
In 16th European Symposium on Programming (ESOP '07), pp. 189-204,
Braga, Portugal, March 2007.
Extended version: Harvard University Technical Report TR-14-06, September 2006.

Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types.
Amal Ahmed.
In 15th European Symposium on Programming (ESOP '06), pp. 69-83, Vienna, Austria, March 2006.
Extended version: Harvard University Technical Report TR-01-06, March 2006.

Linear Regions Are All You Need.
Matthew Fluet, Greg Morrisett, and Amal Ahmed.
In 15th European Symposium on Programming (ESOP '06), pp. 7-21, Vienna, Austria, March 2006.

A Step-Indexed Model of Substructural State.
Amal Ahmed, Matthew Fluet, and Greg Morrisett.
In 10th ACM SIGPLAN International Conference on Functional Programming (ICFP '05), pp. 78-91, Tallinn, Estonia, September 2005.
Extended version: Harvard University Technical Report TR-16-05, February 2005.

L3: A Linear Language with Locations.
Greg Morrisett, Amal Ahmed, and Matthew Fluet.
In 7th International Conference on Typed Lambda Calculi and Applications (TLCA '05), Nara, Japan, LNCS 3461, pp. 293-307, Springer-Verlag, April 2005.
[ For more detailed discussion, examples, and proofs, see the technical report below. ]

L3: A Linear Language with Locations.
Amal Ahmed, Matthew Fluet, and Greg Morrisett.
Harvard University Technical Report TR-24-04, July 2004.

Semantics of Types for Mutable State.
Amal Jamil Ahmed.
PhD thesis, Princeton University, 2004.
[ Official version : Double-Spc (246 pp) pdf | ps ] [ Tree-friendly version : Single-Spc (178 pp) pdf | ps ].

An Indexed Model of Impredicative Polymorphism and Mutable References.
Amal Ahmed, Andrew W. Appel, and Roberto Virga.
Draft of January 2003.

Reasoning about Hierarchical Storage.
Amal Ahmed, Limin Jia, and David Walker.
In 18th Annual IEEE Symposium on Logic in Computer Science (LICS '03), pp. 33-44, Ottawa, Canada, June 2003.

The Logical Approach to Stack Typing.
Amal Ahmed and David Walker.
In ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI '03), pp. 74-85, New Orleans, Louisiana, USA, January 2003.

A Stratified Semantics of General References Embeddable in Higher-Order Logic.
Amal Ahmed, Andrew W. Appel, and Roberto Virga.
In 17th Annual IEEE Symposium on Logic in Computer Science (LICS '02), pp. 75-86, Copenhagen, Denmark, July 2002.

Modeling Collections of Changing Interdependent Objects.
Amal Ahmed, Diane Litman, Anil Mishra, Peter F. Patel-Schneider, and Johannes P. Ros.
In Implementing Application Frameworks: Object-Oriented Frameworks at Work, Mohamed E. Fayad, Douglas C. Schmidt, Ralph Johnson (Editors), John Wiley & Sons, September 1999.