| 2024 | LICS | A Nominal Approach to Probabilistic Separation Logic. | John M. Li, Jon Aytac, Philip Johnson-Freyd, Amal Ahmed, Steven Holtzen |
| 2023 | ICFP | Semantic Encapsulation using Linking Types. | Daniel Patterson, Andrew Wagner, Amal Ahmed |
| 2022 | PLDI | Semantic soundness for language interoperability. | Daniel Patterson, Noble Mushtak, Andrew Wagner, Amal Ahmed |
| 2019 | PPDP | Under Control: Compositionally Correct Closure Conversion with Mutable State. | Phillip Mates, Jamie Perconti, Amal Ahmed |
| 2018 | FOSSACS | Fab ous Interoperability for ML and a Linear Language. | Gabriel Scherer, Max S. New, Nick Rioux, Amal Ahmed |
| 2018 | PLDI | Typed closure conversion for the calculus of constructions. | William J. Bowman, Amal Ahmed |
| 2017 | PLDI | FunTAL: reasonably mixing a functional language with assembly. | Daniel Patterson, Jamie Perconti, Christos Dimoulas, Amal Ahmed |
| 2016 | ICFP | Fully abstract compilation via universal embedding. | Max S. New, William J. Bowman, Amal Ahmed |
| 2015 | ICFP | Noninterference for free. | William J. Bowman, Amal Ahmed |
| 2014 | ESOP | Verifying an Open Compiler Using Multi-language Semantics. | James T. Perconti, Amal Ahmed |
| 2014 | PPDP | Database Queries that Explain their Work. | James Cheney, Amal Ahmed, Umut A. Acar |
| 2013 | POPL | Logical relations for fine-grained concurrency. | Aaron Joseph Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, Derek Dreyer |
| 2011 | ICFP | An equivalence-preserving CPS translation via multi-language semantics. | Amal Ahmed, Matthias Blume |
| 2011 | POPL | Blame for all. | Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, Philip Wadler |
| 2009 | ECOOP | Blame for all. | Amal Ahmed, Robert Bruce Findler, Jacob Matthews, Philip Wadler |
| 2009 | LICS | Logical Step-Indexed Logical Relations. | Derek Dreyer, Amal Ahmed, Lars Birkedal |
| 2009 | POPL | State-dependent representation independence. | Amal Ahmed, Derek Dreyer, Andreas Rossberg |
| 2008 | ESOP | Parametric Polymorphism through Run-Time Sealing or, Theorems for Low, Low Prices!. | Jacob Matthews, Amal Ahmed |
| 2008 | ICFP | Typed closure conversion preserves observational equivalence. | Amal Ahmed, Matthias Blume |
| 2008 | POPL | Imperative self-adjusting computation. | Umut A. Acar, Amal Ahmed, Matthias Blume |
| 2007 | ESOP | Abstract Predicates and Mutable ADTs in Hoare Type Theory. | Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, Lars Birkedal |